From ef1c6c0e5499a83be7f86ccf64e3eb8814137cc9 Mon Sep 17 00:00:00 2001 From: Claire Dross Date: Mon, 19 Aug 2019 08:35:53 +0000 Subject: [PATCH] [Ada] Allow reading a borrowed object inside a call to a pledge function No impact on regular compilation. 2019-08-19 Claire Dross 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 --- gcc/ada/ChangeLog | 10 ++++++++++ gcc/ada/sem_spark.adb | 36 ++++++++++++++++++++++++++++++++++++ gcc/ada/sem_spark.ads | 3 +++ 3 files changed, 49 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8ba0dc4a1d2..d06fd4ef53a 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,13 @@ +2019-08-19 Claire Dross + + * 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 * libgnat/a-cfdlli.ads, libgnat/a-cfhama.ads, diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index b0686b798fc..30e14267747 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 7c16281b9a2..0aaa11584ba 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; -- 2.30.2