From 179682a55cbe229442cf3886e338148be0b12a96 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 10 Jul 2019 09:02:42 +0000 Subject: [PATCH] [Ada] Fix spurious messages on global variables for SPARK pointer support Pointer support in GNATprove leads to spurious messages about global variables, with local variables declared in local packages and protected components. Now fixed. There is no impact on compilation. 2019-07-10 Yannick Moy gcc/ada/ * sem_aux.adb, sem_aux.ads (Is_Protected_Operation): New function to determine if a subprogram is protected. * sem_spark.adb (Setup_Protected_Components): New procedure to add protected components to the environment. (Check_Callable_Body): Call the new Setup_Protected_Components. (Check_Package_Spec): Merge local environment with enclosing one when done. From-SVN: r273349 --- gcc/ada/ChangeLog | 10 +++++++++ gcc/ada/sem_aux.adb | 12 ++++++++++ gcc/ada/sem_aux.ads | 4 ++++ gcc/ada/sem_spark.adb | 52 +++++++++++++++++++++++++++++++++++++++++-- 4 files changed, 76 insertions(+), 2 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 2ef2faf627a..e781181583e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,13 @@ +2019-07-10 Yannick Moy + + * sem_aux.adb, sem_aux.ads (Is_Protected_Operation): New + function to determine if a subprogram is protected. + * sem_spark.adb (Setup_Protected_Components): New procedure to + add protected components to the environment. + (Check_Callable_Body): Call the new Setup_Protected_Components. + (Check_Package_Spec): Merge local environment with enclosing one + when done. + 2019-07-10 Claire Dross * sem_spark.adb (Check_Expression): Allow digits constraints as diff --git a/gcc/ada/sem_aux.adb b/gcc/ada/sem_aux.adb index 09540325082..6a93a3970e9 100644 --- a/gcc/ada/sem_aux.adb +++ b/gcc/ada/sem_aux.adb @@ -1324,6 +1324,18 @@ package body Sem_Aux is end if; end Is_Limited_View; + ---------------------------- + -- Is_Protected_Operation -- + ---------------------------- + + function Is_Protected_Operation (E : Entity_Id) return Boolean is + begin + return Is_Entry (E) + or else (Is_Subprogram (E) + and then Nkind (Parent (Unit_Declaration_Node (E))) = + N_Protected_Definition); + end Is_Protected_Operation; + ---------------------- -- Nearest_Ancestor -- ---------------------- diff --git a/gcc/ada/sem_aux.ads b/gcc/ada/sem_aux.ads index f3b7f2469ff..55cfefa92a3 100644 --- a/gcc/ada/sem_aux.ads +++ b/gcc/ada/sem_aux.ads @@ -357,6 +357,10 @@ package Sem_Aux is -- these types). This older routine overlaps with the previous one, this -- should be cleaned up??? + function Is_Protected_Operation (E : Entity_Id) return Boolean; + -- Given a subprogram or entry, determines whether E is a protected entry + -- or subprogram. + function Nearest_Ancestor (Typ : Entity_Id) return Entity_Id; -- Given a subtype Typ, this function finds out the nearest ancestor from -- which constraints and predicates are inherited. There is no simple link diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index 150433321ee..10c82fffc73 100644 --- a/gcc/ada/sem_spark.adb +++ b/gcc/ada/sem_spark.adb @@ -876,6 +876,10 @@ package body Sem_SPARK is -- Takes a subprogram as input, and sets up the environment by adding -- formal parameters with appropriate permissions. + procedure Setup_Protected_Components (Subp : Entity_Id); + -- Takes a protected operation as input, and sets up the environment by + -- adding protected components with appropriate permissions. + ---------------------- -- Global Variables -- ---------------------- @@ -1336,6 +1340,13 @@ package body Sem_SPARK is Setup_Globals (Spec_Id); end if; + -- For protected operations, add protected components to the environment + -- with adequate permissions. + + if Is_Protected_Operation (Spec_Id) then + Setup_Protected_Components (Spec_Id); + end if; + -- Analyze the body of the subprogram Check_List (Declarations (Body_N)); @@ -2634,9 +2645,13 @@ package body Sem_SPARK is Check_List (Private_Declarations (Spec)); end if; - -- Restore the saved environment and free the current one + -- Restore the saved environment and free the current one. As part of + -- the restoration, the environment of the package spec is merged in + -- the enclosing environment, which may be an enclosing + -- package/subprogram spec or body which has access to the variables + -- of the package spec. - Move_Env (Saved_Env, Current_Perm_Env); + Merge_Env (Saved_Env, Current_Perm_Env); Inside_Elaboration := Save_In_Elab; end if; @@ -5418,4 +5433,37 @@ package body Sem_SPARK is end loop; end Setup_Parameters; + -------------------------------- + -- Setup_Protected_Components -- + -------------------------------- + + procedure Setup_Protected_Components (Subp : Entity_Id) is + Typ : constant Entity_Id := Scope (Subp); + Comp : Entity_Id; + Kind : Formal_Kind; + + begin + Comp := First_Component_Or_Discriminant (Typ); + + -- The protected object is an implicit input of protected functions, and + -- an implicit input-output of protected procedures and entries. + + if Ekind (Subp) = E_Function then + Kind := E_In_Parameter; + else + Kind := E_In_Out_Parameter; + end if; + + while Present (Comp) loop + Setup_Parameter_Or_Global + (Id => Comp, + Typ => Underlying_Type (Etype (Comp)), + Kind => Kind, + Subp => Subp, + Global_Var => False, + Expl => Comp); + Next_Component_Or_Discriminant (Comp); + end loop; + end Setup_Protected_Components; + end Sem_SPARK; -- 2.30.2