Commit 179682a5 by Yannick Moy Committed by Pierre-Marie de Rodat

[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  <moy@adacore.com>

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
parent 1bc68e0d
2019-07-10 Yannick Moy <moy@adacore.com>
* 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 <dross@adacore.com> 2019-07-10 Claire Dross <dross@adacore.com>
* sem_spark.adb (Check_Expression): Allow digits constraints as * sem_spark.adb (Check_Expression): Allow digits constraints as
......
...@@ -1324,6 +1324,18 @@ package body Sem_Aux is ...@@ -1324,6 +1324,18 @@ package body Sem_Aux is
end if; end if;
end Is_Limited_View; 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 -- -- Nearest_Ancestor --
---------------------- ----------------------
......
...@@ -357,6 +357,10 @@ package Sem_Aux is ...@@ -357,6 +357,10 @@ package Sem_Aux is
-- these types). This older routine overlaps with the previous one, this -- these types). This older routine overlaps with the previous one, this
-- should be cleaned up??? -- 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; function Nearest_Ancestor (Typ : Entity_Id) return Entity_Id;
-- Given a subtype Typ, this function finds out the nearest ancestor from -- Given a subtype Typ, this function finds out the nearest ancestor from
-- which constraints and predicates are inherited. There is no simple link -- which constraints and predicates are inherited. There is no simple link
......
...@@ -876,6 +876,10 @@ package body Sem_SPARK is ...@@ -876,6 +876,10 @@ package body Sem_SPARK is
-- Takes a subprogram as input, and sets up the environment by adding -- Takes a subprogram as input, and sets up the environment by adding
-- formal parameters with appropriate permissions. -- 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 -- -- Global Variables --
---------------------- ----------------------
...@@ -1336,6 +1340,13 @@ package body Sem_SPARK is ...@@ -1336,6 +1340,13 @@ package body Sem_SPARK is
Setup_Globals (Spec_Id); Setup_Globals (Spec_Id);
end if; 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 -- Analyze the body of the subprogram
Check_List (Declarations (Body_N)); Check_List (Declarations (Body_N));
...@@ -2634,9 +2645,13 @@ package body Sem_SPARK is ...@@ -2634,9 +2645,13 @@ package body Sem_SPARK is
Check_List (Private_Declarations (Spec)); Check_List (Private_Declarations (Spec));
end if; 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; Inside_Elaboration := Save_In_Elab;
end if; end if;
...@@ -5418,4 +5433,37 @@ package body Sem_SPARK is ...@@ -5418,4 +5433,37 @@ package body Sem_SPARK is
end loop; end loop;
end Setup_Parameters; 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; end Sem_SPARK;
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment