===================================================================
@@ -2513,6 +2513,13 @@
Remove_Visible_Refinements (Corresponding_Spec (Context));
end if;
+
+ -- Verify that all abstract states found in any package declared in
+ -- the input declarative list have proper refinements. The check is
+ -- performed only when the context denotes a block, entry, package,
+ -- protected, subprogram, or task body (SPARK RM 7.2.2(3)).
+
+ Check_State_Refinements (Context);
end if;
end Analyze_Declarations;
===================================================================
@@ -140,11 +140,13 @@
-- tightened further???
function Requires_Completion_In_Body
- (Id : Entity_Id;
- Pack_Id : Entity_Id) return Boolean;
+ (Id : Entity_Id;
+ Pack_Id : Entity_Id;
+ Do_Abstract_States : Boolean := False) return Boolean;
-- Subsidiary to routines Unit_Requires_Body and Unit_Requires_Body_Info.
-- Determine whether entity Id declared in package spec Pack_Id requires
- -- completion in a package body.
+ -- completion in a package body. Flag Do_Abstract_Stats should be set when
+ -- abstract states are to be considered in the completion test.
procedure Unit_Requires_Body_Info (Pack_Id : Entity_Id);
-- Outputs info messages showing why package Pack_Id requires a body. The
@@ -940,15 +942,12 @@
Id : constant Node_Id := Defining_Entity (N);
Par : constant Node_Id := Parent_Spec (N);
+ Is_Comp_Unit : constant Boolean :=
+ Nkind (Parent (N)) = N_Compilation_Unit;
+
Body_Required : Boolean;
-- True when this package declaration requires a corresponding body
- Comp_Unit : Boolean;
- -- True when this package declaration is not a nested declaration
-
- PF : Boolean;
- -- True when in the context of a declared pure library unit
-
begin
if Debug_Flag_C then
Write_Str ("==> package spec ");
@@ -990,9 +989,9 @@
Analyze_Aspect_Specifications (N, Id);
end if;
- -- Ada 2005 (AI-217): Check if the package has been illegally named
- -- in a limited-with clause of its own context. In this case the error
- -- has been previously notified by Analyze_Context.
+ -- Ada 2005 (AI-217): Check if the package has been illegally named in
+ -- a limited-with clause of its own context. In this case the error has
+ -- been previously notified by Analyze_Context.
-- limited with Pkg; -- ERROR
-- package Pkg is ...
@@ -1003,31 +1002,46 @@
Push_Scope (Id);
- PF := Is_Pure (Enclosing_Lib_Unit_Entity);
- Set_Is_Pure (Id, PF);
-
+ Set_Is_Pure (Id, Is_Pure (Enclosing_Lib_Unit_Entity));
Set_Categorization_From_Pragmas (N);
Analyze (Specification (N));
Validate_Categorization_Dependency (N, Id);
+ -- Determine whether the package requires a body. Abstract states are
+ -- intentionally ignored because they do require refinement which can
+ -- only come in a body, but at the same time they do not force the need
+ -- for a body on their own (SPARK RM 7.1.4(4) and 7.2.2(3)).
+
Body_Required := Unit_Requires_Body (Id);
- -- When this spec does not require an explicit body, we know that there
- -- are no entities requiring completion in the language sense; we call
- -- Check_Completion here only to ensure that any nested package
- -- declaration that requires an implicit body gets one. (In the case
- -- where a body is required, Check_Completion is called at the end of
- -- the body's declarative part.)
+ if not Body_Required then
- if not Body_Required then
+ -- If the package spec does not require an explicit body, then there
+ -- are not entities requiring completion in the language sense. Call
+ -- Check_Completion now to ensure that nested package declarations
+ -- that require an implicit body get one. (In the case where a body
+ -- is required, Check_Completion is called at the end of the body's
+ -- declarative part.)
+
Check_Completion;
+
+ -- If the package spec does not require an explicit body, then all
+ -- abstract states declared in nested packages cannot possibly get
+ -- a proper refinement (SPARK RM 7.2.2(3)). This check is performed
+ -- only when the compilation unit is the main unit to allow for
+ -- modular SPARK analysis where packages do not necessarily have
+ -- bodies.
+
+ if Is_Comp_Unit then
+ Check_State_Refinements
+ (Context => N,
+ Is_Main_Unit => Parent (N) = Cunit (Main_Unit));
+ end if;
end if;
- Comp_Unit := Nkind (Parent (N)) = N_Compilation_Unit;
+ if Is_Comp_Unit then
- if Comp_Unit then
-
-- Set Body_Required indication on the compilation unit node, and
-- determine whether elaboration warnings may be meaningful on it.
@@ -1046,7 +1060,7 @@
-- visibility tests that rely on the fact that we have exited the scope
-- of Id.
- if Comp_Unit then
+ if Is_Comp_Unit then
Validate_RT_RAT_Component (N);
end if;
@@ -2439,8 +2453,9 @@
---------------------------------
function Requires_Completion_In_Body
- (Id : Entity_Id;
- Pack_Id : Entity_Id) return Boolean
+ (Id : Entity_Id;
+ Pack_Id : Entity_Id;
+ Do_Abstract_States : Boolean := False) return Boolean
is
begin
-- Always ignore child units. Child units get added to the entity list
@@ -2473,7 +2488,7 @@
(Ekind (Id) = E_Package
and then Id /= Pack_Id
and then not Has_Completion (Id)
- and then Unit_Requires_Body (Id))
+ and then Unit_Requires_Body (Id, Do_Abstract_States))
or else
(Ekind (Id) = E_Incomplete_Type
@@ -2488,7 +2503,7 @@
(Ekind (Id) = E_Generic_Package
and then Id /= Pack_Id
and then not Has_Completion (Id)
- and then Unit_Requires_Body (Id))
+ and then Unit_Requires_Body (Id, Do_Abstract_States))
or else
(Is_Generic_Subprogram (Id)
@@ -2955,8 +2970,8 @@
------------------------
function Unit_Requires_Body
- (Pack_Id : Entity_Id;
- Ignore_Abstract_State : Boolean := False) return Boolean
+ (Pack_Id : Entity_Id;
+ Do_Abstract_States : Boolean := False) return Boolean
is
E : Entity_Id;
@@ -3012,7 +3027,9 @@
if Ekind (E) = E_Abstract_State then
null;
- elsif Requires_Completion_In_Body (E, Pack_Id) then
+ elsif Requires_Completion_In_Body
+ (E, Pack_Id, Do_Abstract_States)
+ then
Requires_Body := True;
exit;
end if;
@@ -3025,7 +3042,7 @@
-- a completion in a body (SPARK RM 7.1.4(4) and (6)). This check is not
-- performed if the caller requests this behavior.
- if not Ignore_Abstract_State
+ if Do_Abstract_States
and then Ekind_In (Pack_Id, E_Generic_Package, E_Package)
and then Has_Non_Null_Abstract_State (Pack_Id)
and then Requires_Body
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -53,17 +53,14 @@
-- child for public child packages.
function Unit_Requires_Body
- (Pack_Id : Entity_Id;
- Ignore_Abstract_State : Boolean := False) return Boolean;
+ (Pack_Id : Entity_Id;
+ Do_Abstract_States : Boolean := False) return Boolean;
-- Determine whether package Pack_Id requires a body. A specification needs
-- a body if it contains declarations that require completion in the body.
-- A non-Ghost [generic] package does not require a body when it declares
- -- Ghost entities exclusively. If flag Ignore_Abstract_State is True, then
- -- the test for a non-null abstract state (which normally requires a body)
- -- is not carried out. The flag is not currently used, but may be useful
- -- in the future if we implement a compatibility mode which warns about
- -- possible incompatibilities if a SPARK 2014 program is compiled with a
- -- SPARK-unaware compiler.
+ -- Ghost entities exclusively. When flag Do_Abstract_States is set to True,
+ -- non-null abstract states are considered in determining the need for a
+ -- body.
procedure May_Need_Implicit_Body (E : Entity_Id);
-- If a package declaration contains tasks or RACWs and does not require
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -2685,7 +2685,6 @@
Enter_Name (Obj_Id);
Set_Ekind (Obj_Id, E_Variable);
Set_Etype (Obj_Id, Typ);
- Set_Part_Of_Constituents (Obj_Id, New_Elmt_List);
Set_SPARK_Pragma (Obj_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Obj_Id);
@@ -2772,7 +2771,6 @@
Enter_Name (Obj_Id);
Set_Ekind (Obj_Id, E_Variable);
Set_Etype (Obj_Id, Typ);
- Set_Part_Of_Constituents (Obj_Id, New_Elmt_List);
Set_SPARK_Pragma (Obj_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Obj_Id);
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -5613,12 +5613,10 @@
procedure Decorate_State (Ent : Entity_Id; Scop : Entity_Id) is
begin
- Set_Ekind (Ent, E_Abstract_State);
- Set_Etype (Ent, Standard_Void_Type);
- Set_Scope (Ent, Scop);
- Set_Encapsulating_State (Ent, Empty);
- Set_Refinement_Constituents (Ent, New_Elmt_List);
- Set_Part_Of_Constituents (Ent, New_Elmt_List);
+ Set_Ekind (Ent, E_Abstract_State);
+ Set_Etype (Ent, Standard_Void_Type);
+ Set_Scope (Ent, Scop);
+ Set_Encapsulating_State (Ent, Empty);
end Decorate_State;
-------------------
===================================================================
@@ -7351,22 +7351,21 @@
-------------------------------------
function Has_Non_Null_Visible_Refinement (Id : E) return B is
+ Constits : Elist_Id;
+
begin
-- "Refinement" is a concept applicable only to abstract states
pragma Assert (Ekind (Id) = E_Abstract_State);
+ Constits := Refinement_Constituents (Id);
- if Has_Visible_Refinement (Id) then
- pragma Assert (Present (Refinement_Constituents (Id)));
+ -- For a refinement to be non-null, the first constituent must be
+ -- anything other than null.
- -- For a refinement to be non-null, the first constituent must be
- -- anything other than null.
-
- return
- Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) /= N_Null;
- end if;
-
- return False;
+ return
+ Has_Visible_Refinement (Id)
+ and then Present (Constits)
+ and then Nkind (Node (First_Elmt (Constits))) /= N_Null;
end Has_Non_Null_Visible_Refinement;
-----------------------------
@@ -7387,22 +7386,21 @@
---------------------------------
function Has_Null_Visible_Refinement (Id : E) return B is
+ Constits : Elist_Id;
+
begin
-- "Refinement" is a concept applicable only to abstract states
pragma Assert (Ekind (Id) = E_Abstract_State);
+ Constits := Refinement_Constituents (Id);
- if Has_Visible_Refinement (Id) then
- pragma Assert (Present (Refinement_Constituents (Id)));
+ -- For a refinement to be null, the state's sole constituent must be a
+ -- null.
- -- For a refinement to be null, the state's sole constituent must be
- -- a null.
-
- return
- Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) = N_Null;
- end if;
-
- return False;
+ return
+ Has_Visible_Refinement (Id)
+ and then Present (Constits)
+ and then Nkind (Node (First_Elmt (Constits))) = N_Null;
end Has_Null_Visible_Refinement;
--------------------
===================================================================
@@ -3342,6 +3342,7 @@
Errors : constant Nat := Serious_Errors_Detected;
Var_Decl : constant Node_Id := Find_Related_Context (N);
Var_Id : constant Entity_Id := Defining_Entity (Var_Decl);
+ Constits : Elist_Id;
Encap_Id : Entity_Id;
Legal : Boolean;
@@ -3362,8 +3363,14 @@
if Legal then
pragma Assert (Present (Encap_Id));
+ Constits := Part_Of_Constituents (Encap_Id);
- Append_Elmt (Var_Id, Part_Of_Constituents (Encap_Id));
+ if No (Constits) then
+ Constits := New_Elmt_List;
+ Set_Part_Of_Constituents (Encap_Id, Constits);
+ end if;
+
+ Append_Elmt (Var_Id, Constits);
Set_Encapsulating_State (Var_Id, Encap_Id);
end if;
@@ -10568,6 +10575,7 @@
procedure Analyze_Part_Of_Option (Opt : Node_Id) is
Encap : constant Node_Id := Expression (Opt);
+ Constits : Elist_Id;
Encap_Id : Entity_Id;
Legal : Boolean;
@@ -10587,8 +10595,14 @@
if Legal then
pragma Assert (Present (Encap_Id));
+ Constits := Part_Of_Constituents (Encap_Id);
- Append_Elmt (State_Id, Part_Of_Constituents (Encap_Id));
+ if No (Constits) then
+ Constits := New_Elmt_List;
+ Set_Part_Of_Constituents (Encap_Id, Constits);
+ end if;
+
+ Append_Elmt (State_Id, Constits);
Set_Encapsulating_State (State_Id, Encap_Id);
end if;
end Analyze_Part_Of_Option;
@@ -10670,13 +10684,11 @@
-- Null states never come from source
- Set_Comes_From_Source (State_Id, not Is_Null);
- Set_Parent (State_Id, State);
- Set_Ekind (State_Id, E_Abstract_State);
- Set_Etype (State_Id, Standard_Void_Type);
- Set_Encapsulating_State (State_Id, Empty);
- Set_Refinement_Constituents (State_Id, New_Elmt_List);
- Set_Part_Of_Constituents (State_Id, New_Elmt_List);
+ Set_Comes_From_Source (State_Id, not Is_Null);
+ Set_Parent (State_Id, State);
+ Set_Ekind (State_Id, E_Abstract_State);
+ Set_Etype (State_Id, Standard_Void_Type);
+ Set_Encapsulating_State (State_Id, Empty);
-- An abstract state declared within a Ghost region becomes
-- Ghost (SPARK RM 6.9(2)).
@@ -18193,7 +18205,8 @@
-----------------------
procedure Propagate_Part_Of (Pack_Id : Entity_Id) is
- Item_Id : Entity_Id;
+ Constits : Elist_Id;
+ Item_Id : Entity_Id;
begin
-- Traverse the entity chain of the package and set relevant
@@ -18217,8 +18230,14 @@
E_Variable)
then
Has_Item := True;
+ Constits := Part_Of_Constituents (State_Id);
- Append_Elmt (Item_Id, Part_Of_Constituents (State_Id));
+ if No (Constits) then
+ Constits := New_Elmt_List;
+ Set_Part_Of_Constituents (State_Id, Constits);
+ end if;
+
+ Append_Elmt (Item_Id, Constits);
Set_Encapsulating_State (Item_Id, State_Id);
-- Recursively handle nested packages and instantiations
@@ -18248,6 +18267,7 @@
-- Local variables
+ Constits : Elist_Id;
Encap : Node_Id;
Encap_Id : Entity_Id;
Item_Id : Entity_Id;
@@ -18334,7 +18354,14 @@
pragma Assert (Present (Encap_Id));
if Ekind (Item_Id) = E_Constant then
- Append_Elmt (Item_Id, Part_Of_Constituents (Encap_Id));
+ Constits := Part_Of_Constituents (Encap_Id);
+
+ if No (Constits) then
+ Constits := New_Elmt_List;
+ Set_Part_Of_Constituents (Encap_Id, Constits);
+ end if;
+
+ Append_Elmt (Item_Id, Constits);
Set_Encapsulating_State (Item_Id, Encap_Id);
-- Propagate the Part_Of indicator to the visible state
@@ -23657,7 +23684,7 @@
-- the pool of candidates. The seach continues because a single
-- dependence clause may have multiple matching refinements.
- if Inputs_Match and then Outputs_Match then
+ if Inputs_Match and Outputs_Match then
Clause_Matched := True;
Remove (Ref_Clause);
end if;
@@ -23769,45 +23796,49 @@
-----------------------------
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
+ Constits : constant Elist_Id :=
+ Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Posted : Boolean := False;
begin
- Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id));
- while Present (Constit_Elmt) loop
- Constit_Id := Node (Constit_Elmt);
+ if Present (Constits) then
+ Constit_Elmt := First_Elmt (Constits);
+ while Present (Constit_Elmt) loop
+ Constit_Id := Node (Constit_Elmt);
- -- The constituent acts as an input (SPARK RM 7.2.5(3))
+ -- The constituent acts as an input (SPARK RM 7.2.5(3))
- if Present (Body_Inputs)
- and then Appears_In (Body_Inputs, Constit_Id)
- then
- Error_Msg_Name_1 := Chars (State_Id);
- SPARK_Msg_NE
- ("constituent & of state % must act as output in "
- & "dependence refinement", N, Constit_Id);
+ if Present (Body_Inputs)
+ and then Appears_In (Body_Inputs, Constit_Id)
+ then
+ Error_Msg_Name_1 := Chars (State_Id);
+ SPARK_Msg_NE
+ ("constituent & of state % must act as output in "
+ & "dependence refinement", N, Constit_Id);
- -- The constituent is altogether missing (SPARK RM 7.2.5(3))
+ -- The constituent is altogether missing (SPARK RM 7.2.5(3))
- elsif No (Body_Outputs)
- or else not Appears_In (Body_Outputs, Constit_Id)
- then
- if not Posted then
- Posted := True;
+ elsif No (Body_Outputs)
+ or else not Appears_In (Body_Outputs, Constit_Id)
+ then
+ if not Posted then
+ Posted := True;
+ SPARK_Msg_NE
+ ("output state & must be replaced by all its "
+ & "constituents in dependence refinement",
+ N, State_Id);
+ end if;
+
SPARK_Msg_NE
- ("output state & must be replaced by all its "
- & "constituents in dependence refinement",
- N, State_Id);
+ ("\constituent & is missing in output list",
+ N, Constit_Id);
end if;
- SPARK_Msg_NE
- ("\constituent & is missing in output list",
- N, Constit_Id);
- end if;
-
- Next_Elmt (Constit_Elmt);
- end loop;
+ Next_Elmt (Constit_Elmt);
+ end loop;
+ end if;
end Check_Constituent_Usage;
-- Local variables
@@ -24328,6 +24359,8 @@
-----------------------------
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
+ Constits : constant Elist_Id :=
+ Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Has_Missing : Boolean := False;
@@ -24340,28 +24373,31 @@
-- Process all the constituents of the state and note their modes
-- within the global refinement.
- Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id));
- while Present (Constit_Elmt) loop
- Constit_Id := Node (Constit_Elmt);
+ if Present (Constits) then
+ Constit_Elmt := First_Elmt (Constits);
+ while Present (Constit_Elmt) loop
+ Constit_Id := Node (Constit_Elmt);
- if Present_Then_Remove (In_Constits, Constit_Id) then
- Input_Seen := True;
+ if Present_Then_Remove (In_Constits, Constit_Id) then
+ Input_Seen := True;
- elsif Present_Then_Remove (In_Out_Constits, Constit_Id) then
- In_Out_Seen := True;
+ elsif Present_Then_Remove (In_Out_Constits, Constit_Id) then
+ In_Out_Seen := True;
- elsif Present_Then_Remove (Out_Constits, Constit_Id) then
- Output_Seen := True;
+ elsif Present_Then_Remove (Out_Constits, Constit_Id) then
+ Output_Seen := True;
- elsif Present_Then_Remove (Proof_In_Constits, Constit_Id) then
- Proof_In_Seen := True;
+ elsif Present_Then_Remove (Proof_In_Constits, Constit_Id)
+ then
+ Proof_In_Seen := True;
- else
- Has_Missing := True;
- end if;
+ else
+ Has_Missing := True;
+ end if;
- Next_Elmt (Constit_Elmt);
- end loop;
+ Next_Elmt (Constit_Elmt);
+ end loop;
+ end if;
-- An In_Out constituent is a valid completion
@@ -24462,40 +24498,45 @@
-----------------------------
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
+ Constits : constant Elist_Id :=
+ Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
In_Seen : Boolean := False;
begin
- Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id));
- while Present (Constit_Elmt) loop
- Constit_Id := Node (Constit_Elmt);
+ if Present (Constits) then
+ Constit_Elmt := First_Elmt (Constits);
+ while Present (Constit_Elmt) loop
+ Constit_Id := Node (Constit_Elmt);
- -- At least one of the constituents appears as an Input
+ -- At least one of the constituents appears as an Input
- if Present_Then_Remove (In_Constits, Constit_Id) then
- In_Seen := True;
+ if Present_Then_Remove (In_Constits, Constit_Id) then
+ In_Seen := True;
- -- A Proof_In constituent can refine an Input state as long as
- -- there is at least one Input constituent present.
+ -- A Proof_In constituent can refine an Input state as long
+ -- as there is at least one Input constituent present.
- elsif Present_Then_Remove (Proof_In_Constits, Constit_Id) then
- null;
+ elsif Present_Then_Remove (Proof_In_Constits, Constit_Id)
+ then
+ null;
- -- The constituent appears in the global refinement, but has
- -- mode In_Out or Output (SPARK RM 7.2.4(5)).
+ -- The constituent appears in the global refinement, but has
+ -- mode In_Out or Output (SPARK RM 7.2.4(5)).
- elsif Present_Then_Remove (In_Out_Constits, Constit_Id)
- or else Present_Then_Remove (Out_Constits, Constit_Id)
- then
- Error_Msg_Name_1 := Chars (State_Id);
- SPARK_Msg_NE
- ("constituent & of state % must have mode `Input` in "
- & "global refinement", N, Constit_Id);
- end if;
+ elsif Present_Then_Remove (In_Out_Constits, Constit_Id)
+ or else Present_Then_Remove (Out_Constits, Constit_Id)
+ then
+ Error_Msg_Name_1 := Chars (State_Id);
+ SPARK_Msg_NE
+ ("constituent & of state % must have mode `Input` in "
+ & "global refinement", N, Constit_Id);
+ end if;
- Next_Elmt (Constit_Elmt);
- end loop;
+ Next_Elmt (Constit_Elmt);
+ end loop;
+ end if;
-- Not one of the constituents appeared as Input
@@ -24557,47 +24598,51 @@
-----------------------------
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
+ Constits : constant Elist_Id :=
+ Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Posted : Boolean := False;
begin
- Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id));
- while Present (Constit_Elmt) loop
- Constit_Id := Node (Constit_Elmt);
+ if Present (Constits) then
+ Constit_Elmt := First_Elmt (Constits);
+ while Present (Constit_Elmt) loop
+ Constit_Id := Node (Constit_Elmt);
- if Present_Then_Remove (Out_Constits, Constit_Id) then
- null;
+ if Present_Then_Remove (Out_Constits, Constit_Id) then
+ null;
- -- The constituent appears in the global refinement, but has
- -- mode Input, In_Out or Proof_In (SPARK RM 7.2.4(5)).
+ -- The constituent appears in the global refinement, but has
+ -- mode Input, In_Out or Proof_In (SPARK RM 7.2.4(5)).
- elsif Present_Then_Remove (In_Constits, Constit_Id)
- or else Present_Then_Remove (In_Out_Constits, Constit_Id)
- or else Present_Then_Remove (Proof_In_Constits, Constit_Id)
- then
- Error_Msg_Name_1 := Chars (State_Id);
- SPARK_Msg_NE
- ("constituent & of state % must have mode `Output` in "
- & "global refinement", N, Constit_Id);
+ elsif Present_Then_Remove (In_Constits, Constit_Id)
+ or else Present_Then_Remove (In_Out_Constits, Constit_Id)
+ or else Present_Then_Remove (Proof_In_Constits, Constit_Id)
+ then
+ Error_Msg_Name_1 := Chars (State_Id);
+ SPARK_Msg_NE
+ ("constituent & of state % must have mode `Output` in "
+ & "global refinement", N, Constit_Id);
- -- The constituent is altogether missing (SPARK RM 7.2.5(3))
+ -- The constituent is altogether missing (SPARK RM 7.2.5(3))
- else
- if not Posted then
- Posted := True;
+ else
+ if not Posted then
+ Posted := True;
+ SPARK_Msg_NE
+ ("`Output` state & must be replaced by all its "
+ & "constituents in global refinement", N, State_Id);
+ end if;
+
SPARK_Msg_NE
- ("`Output` state & must be replaced by all its "
- & "constituents in global refinement", N, State_Id);
+ ("\constituent & is missing in output list",
+ N, Constit_Id);
end if;
- SPARK_Msg_NE
- ("\constituent & is missing in output list",
- N, Constit_Id);
- end if;
-
- Next_Elmt (Constit_Elmt);
- end loop;
+ Next_Elmt (Constit_Elmt);
+ end loop;
+ end if;
end Check_Constituent_Usage;
-- Local variables
@@ -24652,35 +24697,39 @@
-----------------------------
procedure Check_Constituent_Usage (State_Id : Entity_Id) is
+ Constits : constant Elist_Id :=
+ Refinement_Constituents (State_Id);
Constit_Elmt : Elmt_Id;
Constit_Id : Entity_Id;
Proof_In_Seen : Boolean := False;
begin
- Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id));
- while Present (Constit_Elmt) loop
- Constit_Id := Node (Constit_Elmt);
+ if Present (Constits) then
+ Constit_Elmt := First_Elmt (Constits);
+ while Present (Constit_Elmt) loop
+ Constit_Id := Node (Constit_Elmt);
- -- At least one of the constituents appears as Proof_In
+ -- At least one of the constituents appears as Proof_In
- if Present_Then_Remove (Proof_In_Constits, Constit_Id) then
- Proof_In_Seen := True;
+ if Present_Then_Remove (Proof_In_Constits, Constit_Id) then
+ Proof_In_Seen := True;
- -- The constituent appears in the global refinement, but has
- -- mode Input, In_Out or Output (SPARK RM 7.2.4(5)).
+ -- The constituent appears in the global refinement, but has
+ -- mode Input, In_Out or Output (SPARK RM 7.2.4(5)).
- elsif Present_Then_Remove (In_Constits, Constit_Id)
- or else Present_Then_Remove (In_Out_Constits, Constit_Id)
- or else Present_Then_Remove (Out_Constits, Constit_Id)
- then
- Error_Msg_Name_1 := Chars (State_Id);
- SPARK_Msg_NE
- ("constituent & of state % must have mode `Proof_In` in "
- & "global refinement", N, Constit_Id);
- end if;
+ elsif Present_Then_Remove (In_Constits, Constit_Id)
+ or else Present_Then_Remove (In_Out_Constits, Constit_Id)
+ or else Present_Then_Remove (Out_Constits, Constit_Id)
+ then
+ Error_Msg_Name_1 := Chars (State_Id);
+ SPARK_Msg_NE
+ ("constituent & of state % must have mode `Proof_In` "
+ & "in global refinement", N, Constit_Id);
+ end if;
- Next_Elmt (Constit_Elmt);
- end loop;
+ Next_Elmt (Constit_Elmt);
+ end loop;
+ end if;
-- Not one of the constituents appeared as Proof_In
@@ -25340,6 +25389,8 @@
-------------------------
procedure Collect_Constituent is
+ Constits : Elist_Id;
+
begin
-- The Ghost policy in effect at the point of abstract state
-- declaration and constituent must match (SPARK RM 6.9(15))
@@ -25368,7 +25419,14 @@
-- and establish a relation between the refined state and
-- the item.
- Append_Elmt (Constit_Id, Refinement_Constituents (State_Id));
+ Constits := Refinement_Constituents (State_Id);
+
+ if No (Constits) then
+ Constits := New_Elmt_List;
+ Set_Refinement_Constituents (State_Id, Constits);
+ end if;
+
+ Append_Elmt (Constit_Id, Constits);
Set_Encapsulating_State (Constit_Id, State_Id);
-- The state has at least one legal constituent, mark the
@@ -25482,6 +25540,7 @@
-- Local variables
Constit_Id : Entity_Id;
+ Constits : Elist_Id;
-- Start of processing for Analyze_Constituent
@@ -25503,8 +25562,15 @@
-- Collect the constituent in the list of refinement items
- Append_Elmt (Constit, Refinement_Constituents (State_Id));
+ Constits := Refinement_Constituents (State_Id);
+ if No (Constits) then
+ Constits := New_Elmt_List;
+ Set_Refinement_Constituents (State_Id, Constits);
+ end if;
+
+ Append_Elmt (Constit, Constits);
+
-- The state has at least one legal constituent, mark the
-- start of the refinement region. The region ends when the
-- body declarations end (see Analyze_Declarations).
===================================================================
@@ -3621,6 +3621,172 @@
end if;
end Check_Result_And_Post_State;
+ -----------------------------
+ -- Check_State_Refinements --
+ -----------------------------
+
+ procedure Check_State_Refinements
+ (Context : Node_Id;
+ Is_Main_Unit : Boolean := False)
+ is
+ procedure Check_Package (Pack : Node_Id);
+ -- Verify that all abstract states of a [generic] package denoted by its
+ -- declarative node Pack have proper refinement. Recursively verify the
+ -- visible and private declarations of the [generic] package for other
+ -- nested packages.
+
+ procedure Check_Packages_In (Decls : List_Id);
+ -- Seek out [generic] package declarations within declarative list Decls
+ -- and verify the status of their abstract state refinement.
+
+ function SPARK_Mode_Is_Off (N : Node_Id) return Boolean;
+ -- Determine whether construct N is subject to pragma SPARK_Mode Off
+
+ -------------------
+ -- Check_Package --
+ -------------------
+
+ procedure Check_Package (Pack : Node_Id) is
+ Body_Id : constant Entity_Id := Corresponding_Body (Pack);
+ Spec : constant Node_Id := Specification (Pack);
+ States : constant Elist_Id :=
+ Abstract_States (Defining_Entity (Pack));
+
+ State_Elmt : Elmt_Id;
+ State_Id : Entity_Id;
+
+ begin
+ -- Do not verify proper state refinement when the package is subject
+ -- to pragma SPARK_Mode Off because this disables the requirement for
+ -- state refinement.
+
+ if SPARK_Mode_Is_Off (Pack) then
+ null;
+
+ -- State refinement can only occur in a completing packge body. Do
+ -- not verify proper state refinement when the body is subject to
+ -- pragma SPARK_Mode Off because this disables the requirement for
+ -- state refinement.
+
+ elsif Present (Body_Id)
+ and then SPARK_Mode_Is_Off (Unit_Declaration_Node (Body_Id))
+ then
+ null;
+
+ -- Do not verify proper state refinement when the package is an
+ -- instance as this check was already performed in the generic.
+
+ elsif Present (Generic_Parent (Spec)) then
+ null;
+
+ -- Otherwise examine the contents of the package
+
+ else
+ if Present (States) then
+ State_Elmt := First_Elmt (States);
+ while Present (State_Elmt) loop
+ State_Id := Node (State_Elmt);
+
+ -- Emit an error when a non-null state lacks any form of
+ -- refinement.
+
+ if not Is_Null_State (State_Id)
+ and then not Has_Null_Refinement (State_Id)
+ and then not Has_Non_Null_Refinement (State_Id)
+ then
+ Error_Msg_N ("state & requires refinement", State_Id);
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+
+ Check_Packages_In (Visible_Declarations (Spec));
+ Check_Packages_In (Private_Declarations (Spec));
+ end if;
+ end Check_Package;
+
+ -----------------------
+ -- Check_Packages_In --
+ -----------------------
+
+ procedure Check_Packages_In (Decls : List_Id) is
+ Decl : Node_Id;
+
+ begin
+ if Present (Decls) then
+ Decl := First (Decls);
+ while Present (Decl) loop
+ if Nkind_In (Decl, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Check_Package (Decl);
+ end if;
+
+ Next (Decl);
+ end loop;
+ end if;
+ end Check_Packages_In;
+
+ -----------------------
+ -- SPARK_Mode_Is_Off --
+ -----------------------
+
+ function SPARK_Mode_Is_Off (N : Node_Id) return Boolean is
+ Prag : constant Node_Id := SPARK_Pragma (Defining_Entity (N));
+
+ begin
+ return
+ Present (Prag) and then Get_SPARK_Mode_From_Annotation (Prag) = Off;
+ end SPARK_Mode_Is_Off;
+
+ -- Start of processing for Check_State_Refinements
+
+ begin
+ -- A block may declare a nested package
+
+ if Nkind (Context) = N_Block_Statement then
+ Check_Packages_In (Declarations (Context));
+
+ -- An entry, protected, subprogram, or task body may declare a nested
+ -- package.
+
+ elsif Nkind_In (Context, N_Entry_Body,
+ N_Protected_Body,
+ N_Subprogram_Body,
+ N_Task_Body)
+ then
+ -- Do not verify proper state refinement when the body is subject to
+ -- pragma SPARK_Mode Off because this disables the requirement for
+ -- state refinement.
+
+ if not SPARK_Mode_Is_Off (Context) then
+ Check_Packages_In (Declarations (Context));
+ end if;
+
+ -- A package body may declare a nested package
+
+ elsif Nkind (Context) = N_Package_Body then
+ Check_Package (Unit_Declaration_Node (Corresponding_Spec (Context)));
+
+ -- Do not verify proper state refinement when the body is subject to
+ -- pragma SPARK_Mode Off because this disables the requirement for
+ -- state refinement.
+
+ if not SPARK_Mode_Is_Off (Context) then
+ Check_Packages_In (Declarations (Context));
+ end if;
+
+ -- A library level [generic] package may declare a nested package
+
+ elsif Nkind_In (Context, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ and then Is_Main_Unit
+ then
+ Check_Package (Context);
+ end if;
+ end Check_State_Refinements;
+
------------------------------
-- Check_Unprotected_Access --
------------------------------
@@ -6294,9 +6460,9 @@
or else Is_Internal (E)
then
declare
+ Decl : constant Node_Id := Parent (E);
Prev : Entity_Id;
Prev_Vis : Entity_Id;
- Decl : constant Node_Id := Parent (E);
begin
-- If E is an implicit declaration, it cannot be the first
@@ -9329,18 +9495,18 @@
-----------------------------
function Has_Non_Null_Refinement (Id : Entity_Id) return Boolean is
+ Constits : Elist_Id;
+
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
+ Constits := Refinement_Constituents (Id);
-- For a refinement to be non-null, the first constituent must be
-- anything other than null.
- if Present (Refinement_Constituents (Id)) then
- return
- Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) /= N_Null;
- end if;
-
- return False;
+ return
+ Present (Constits)
+ and then Nkind (Node (First_Elmt (Constits))) /= N_Null;
end Has_Non_Null_Refinement;
------------------------
@@ -9438,18 +9604,18 @@
-------------------------
function Has_Null_Refinement (Id : Entity_Id) return Boolean is
+ Constits : Elist_Id;
+
begin
pragma Assert (Ekind (Id) = E_Abstract_State);
+ Constits := Refinement_Constituents (Id);
-- For a refinement to be null, the state's sole constituent must be a
-- null.
- if Present (Refinement_Constituents (Id)) then
- return
- Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) = N_Null;
- end if;
-
- return False;
+ return
+ Present (Constits)
+ and then Nkind (Node (First_Elmt (Constits))) = N_Null;
end Has_Null_Refinement;
-------------------------------
@@ -18259,46 +18425,6 @@
end if;
end Require_Entity;
- -------------------------------
- -- Requires_State_Refinement --
- -------------------------------
-
- function Requires_State_Refinement
- (Spec_Id : Entity_Id;
- Body_Id : Entity_Id) return Boolean
- is
- Prag : constant Node_Id := SPARK_Pragma (Body_Id);
-
- begin
- -- A package that does not define at least one abstract state cannot
- -- possibly require refinement.
-
- if No (Abstract_States (Spec_Id)) then
- return False;
-
- -- The package instroduces a single null state which does not merit
- -- refinement.
-
- elsif Has_Null_Abstract_State (Spec_Id) then
- return False;
-
- -- Check whether the package body is subject to pragma SPARK_Mode. If
- -- it is and the mode is Off, the package body is considered to be in
- -- regular Ada and does not require refinement.
-
- elsif Present (Prag)
- and then Get_SPARK_Mode_From_Annotation (Prag) = Off
- then
- return False;
-
- -- The spec defines at least one abstract state and the body has no way
- -- of circumventing the refinement.
-
- else
- return True;
- end if;
- end Requires_State_Refinement;
-
------------------------------
-- Requires_Transient_Scope --
------------------------------
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -257,10 +257,6 @@
-- not necessarily mean that CE could be raised, but a response of True
-- means that for sure CE cannot be raised.
- procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id);
- -- Verify the legality of reference Ref to variable Var_Id when the
- -- variable is a constituent of a single protected/task type.
-
procedure Check_Dynamically_Tagged_Expression
(Expr : Node_Id;
Typ : Entity_Id;
@@ -322,6 +318,10 @@
-- Verify that the profile of nonvolatile function Func_Id does not contain
-- effectively volatile parameters or return type.
+ procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id);
+ -- Verify the legality of reference Ref to variable Var_Id when the
+ -- variable is a constituent of a single protected/task type.
+
procedure Check_Potentially_Blocking_Operation (N : Node_Id);
-- N is one of the statement forms that is a potentially blocking
-- operation. If it appears within a protected action, emit warning.
@@ -331,6 +331,15 @@
-- 'Result and it contains an expression that evaluates differently in pre-
-- and post-state.
+ procedure Check_State_Refinements
+ (Context : Node_Id;
+ Is_Main_Unit : Boolean := False);
+ -- Verify that all abstract states declared in a block statement, entry
+ -- body, package body, protected body, subprogram body, task body, or a
+ -- package declaration denoted by Context have proper refinement. Emit an
+ -- error if this is not the case. Flag Is_Main_Unit should be set when
+ -- Context denotes the main compilation unit.
+
procedure Check_Unused_Body_States (Body_Id : Entity_Id);
-- Verify that all abstract states and objects declared in the state space
-- of package body Body_Id are used as constituents. Emit an error if this
@@ -2007,12 +2016,6 @@
-- This is used as a defense mechanism against ill-formed trees caused by
-- previous errors (particularly in -gnatq mode).
- function Requires_State_Refinement
- (Spec_Id : Entity_Id;
- Body_Id : Entity_Id) return Boolean;
- -- Determine whether a package denoted by its spec and body entities
- -- requires refinement of abstract states.
-
function Requires_Transient_Scope (Id : Entity_Id) return Boolean;
-- Id is a type entity. The result is True when temporaries of this type
-- need to be wrapped in a transient scope to be reclaimed properly when a
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 2015-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -949,15 +949,6 @@
if Present (Ref_State) then
Analyze_Refined_State_In_Decl_Part (Ref_State, Freeze_Id);
-
- -- State refinement is required when the package declaration defines at
- -- least one abstract state. Null states are not considered. Refinement
- -- is not enforced when SPARK checks are turned off.
-
- elsif SPARK_Mode /= Off
- and then Requires_State_Refinement (Spec_Id, Body_Id)
- then
- Error_Msg_N ("package & requires state refinement", Spec_Id);
end if;
-- Restore the SPARK_Mode of the enclosing context after all delayed