[Ada] Allow reading a borrowed object inside a call to a pledge function

No impact on regular compilation.

2019-08-19  Claire Dross  <dross@adacore.com>

gcc/ada/

	* sem_spark.ads, sem_spark.adb (Is_Pledge_Function): New
	parameter of the generic. Function used to decide whether a
	function is a pledge function.
	(Check_Not_Borrowed): Disable check inside the second parameter
	of a pledge function for the path borrowed by the first
	parameter. Also disable checks for entities inside a Global
	contract.

From-SVN: r274644

3 files changed, 49 insertions, 0 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8ba0dc4..d06fd4e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,13 @@
+2019-08-19  Claire Dross  <dross@adacore.com>
+
+	* sem_spark.ads, sem_spark.adb (Is_Pledge_Function): New
+	parameter of the generic. Function used to decide whether a
+	function is a pledge function.
+	(Check_Not_Borrowed): Disable check inside the second parameter
+	of a pledge function for the path borrowed by the first
+	parameter. Also disable checks for entities inside a Global
+	contract.
+
 2019-08-19  Joffrey Huguet  <huguet@adacore.com>
 
 	* libgnat/a-cfdlli.ads, libgnat/a-cfhama.ads,
diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index b0686b7..30e1426 100644
--- a/gcc/ada/sem_spark.adb
+++ b/gcc/ada/sem_spark.adb
@@ -5008,13 +5008,49 @@ package body Sem_SPARK is
               Get_First_Key (Current_Borrowers);
             Var      : Entity_Id;
             Borrowed : Node_Id;
+            B_Pledge : Entity_Id := Empty;
 
          begin
+            --  Search for a call to a pledge function or a global pragma in
+            --  the parents of Expr.
+
+            declare
+               Call : Node_Id := Expr;
+            begin
+               while Present (Call)
+                 and then
+                   (Nkind (Call) /= N_Function_Call
+                     or else not Is_Pledge_Function (Get_Called_Entity (Call)))
+               loop
+                  --  Do not check for borrowed objects in global contracts
+                  --  ??? However we should keep these objects in the borrowed
+                  --  state when verifying the subprogram so that we can make
+                  --  sure that they are only read inside pledges.
+                  --  ??? There is probably a better way to disable checking of
+                  --  borrows inside global contracts.
+
+                  if Nkind (Call) = N_Pragma
+                    and then Get_Pragma_Id (Pragma_Name (Call)) = Pragma_Global
+                  then
+                     return;
+                  end if;
+
+                  Call := Parent (Call);
+               end loop;
+
+               if Present (Call)
+                 and then Nkind (First_Actual (Call)) in N_Has_Entity
+               then
+                  B_Pledge := Entity (First_Actual (Call));
+               end if;
+            end;
+
             while Key.Present loop
                Var := Key.K;
                Borrowed := Get (Current_Borrowers, Var);
 
                if Is_Prefix_Or_Almost (Pref => Borrowed, Expr => Expr)
+                 and then Var /= B_Pledge
                  and then Emit_Messages
                then
                   Error_Msg_Sloc := Sloc (Borrowed);
diff --git a/gcc/ada/sem_spark.ads b/gcc/ada/sem_spark.ads
index 7c16281..0aaa115 100644
--- a/gcc/ada/sem_spark.ads
+++ b/gcc/ada/sem_spark.ads
@@ -150,6 +150,9 @@ generic
    with function Emit_Messages return Boolean;
    --  Return True when error messages should be emitted.
 
+   with function Is_Pledge_Function (E : Entity_Id) return Boolean;
+   --  Return True if E is annotated with a pledge annotation
+
 package Sem_SPARK is
 
    function Is_Legal (N : Node_Id) return Boolean;