[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8ba0dc4a1d21ac351fe2603fb7bc6060ff75ad3f..d06fd4ef53add7b90895d35c289c187ba45c4c6e 100644 (file)
--- 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 b0686b798fcaccc9f04cbb3e850829e6a3adf59d..30e1426774792ca41c4b3a52089d5010ca5773f4 100644 (file)
--- 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 7c16281b9a2f3feb1841162d2af1de2d657f74a8..0aaa11584badf815b65ea75cb68598c0520f2fe9 100644 (file)
--- 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;