[Ada] Aspect Refined_Global
Arnaud Charlet
charlet@adacore.com
Sun Oct 13 16:36:00 GMT 2013
This patch provides the initial implementation of aspect/pragma Refined_Global.
This construct is intended for formal verification proofs.
The syntax of Refined_Global is as follows:
pragma Refined_Global (GLOBAL_SPECIFICATION);
GLOBAL_SPECIFICATION ::=
null
| GLOBAL_LIST
| MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST}
MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST
MODE_SELECTOR ::= Input | Output | In_Out | Contract_In
GLOBAL_LIST ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM})
GLOBAL_ITEM ::= NAME
The semantics of Refined_Global are as follows:
A Refined_Global aspect shall be specified on a body_stub (if one is present)
or subprogram body if and only if it has a declaration in the visible part of
an enclosing package, the declaration has a Global aspect which denotes a state
abstraction declared by the package and the refinement of the state abstraction
is visible.
A Refined_Global aspect specification shall refine the subprogram's Global
aspect as follows:
For each global_item in the Global aspect which denotes a state abstraction
whose non-null refinement is visible at the point of the Refined_Global
aspect specification, the Refined_Global specification shall include one or
more global_items which denote constituents of that state abstraction.
For each global_item in the Global aspect which denotes a state abstraction
whose null refinement is visible at the point of the Refined_Global aspect
specification, shall be omitted, or if required by the syntax of a
global_specification replaced by a null in the the Refined_Global aspect.
For each global_item in the Global aspect which does not denote such a state
abstraction, the Refined_Global specification shall include exactly one
global_item which denotes the same entity as the global_item in the Global
aspect.
No other global_items shall be included in the Refined_Global aspect
specification.
Global_items in the a Refined_Global aspect specification shall denote distinct
entities.
The mode of each global_item in a Refined_Global aspect shall match that of the
corresponding global_item in the Global aspect unless: the mode_selector
specified in the Global aspect is In_Out; the corresponding global_item of
Global aspect shall denote a state abstraction whose refinement is visible; and
the global_item in the Refined_Global aspect is a constituent of the state
abstraction.
For this special case when the mode_selector is In_Out, the Refined_Global
aspect may denote individual constituents of the state abstraction as Input,
Output, or In_Out (given that the constituent itself may have any of these
mode_selectors) so long as one or more of the following conditions are
satisfied:
at least one of the constituents has a mode_selector of In_Out; or
there is at least one of each of a constituent with a mode_selector of Input
and of Output; or
the Refined_Global aspect does not denote all of the constituents of the
state abstraction and at least one of them has the mode_selector of Output.
If the Global aspect specification references a state abstraction with a
mode_selector of Output whose refinement is visible, then every constituent of
that state abstraction shall be referenced in the Refined_Global aspect
specification.
The legality rules for Global Aspects and External states described in Refined
External States also apply.
------------
-- Source --
------------
-- semantics.ads
package Semantics
with Abstract_State =>
((State_1 with External, Input_Only),
State_2,
(State_3 with External, Output_Only))
is
In_Var : Integer;
In_Out_Var : Integer;
Out_Var : Integer;
procedure OK
with Global =>
(Input => (State_1, In_Var),
In_Out => (State_2, In_Out_Var),
Output => (State_3, Out_Var));
private
Var_1 : Integer;
end Semantics;
-- semantics.adb
package body Semantics
with Refined_State =>
(State_1 => Var_1,
State_2 => (Nested.State_4, Nested.Var_2),
State_3 => Var_3)
is
procedure OK
with Refined_Global =>
(Input => (Var_1, In_Var),
In_Out => (Nested.State_4, Nested.Var_2, In_Out_Var),
Output => (Var_3, Out_Var)) is
begin null; end OK;
package Nested
with Abstract_State => (State_4 with Part_Of => State_2)
is
Var_2 : Integer;
end Nested;
Var_3 : Integer;
package body Nested
with Refined_State => (State_4 => null)
is end Nested;
end Semantics;
-- completions.ads
package Completions is
package Input_State_Checks
with Abstract_State => (Input_State with External, Input_Only)
is
procedure Input_Proc
with Global => (Input => Input_State);
private
Var_1 : Integer;
end Input_State_Checks;
package In_Out_State_Checks
with Abstract_State => In_Out_State
is
procedure In_Out_Proc_1
with Global => (In_Out => In_Out_State);
procedure In_Out_Proc_2
with Global => (In_Out => In_Out_State);
procedure In_Out_Proc_3
with Global => (In_Out => In_Out_State);
procedure In_Out_Proc_4
with Global => (In_Out => In_Out_State);
procedure In_Out_Proc_5
with Global => (In_Out => In_Out_State);
private
Var_1 : Integer;
end In_Out_State_Checks;
package Output_State_Checks
with Abstract_State => (Output_State with External, Output_Only)
is
procedure Output_Proc_1
with Global => (Output => Output_State);
procedure Output_Proc_2
with Global => (Output => Output_State);
private
Var_1 : Integer;
end Output_State_Checks;
end Completions;
-- completions.adb
package body Completions is
package body Input_State_Checks
with Refined_State => (Input_State => (Var_1, Var_2, Var_3))
is
Var_2 : Integer;
Var_3 : Integer;
procedure Input_Proc
with Refined_Global => (Input => (Var_1, Var_3), -- OK
In_Out => Var_2) -- illegal
is begin null; end Input_Proc;
end Input_State_Checks;
package body In_Out_State_Checks
with Refined_State => (In_Out_State => (Var_1, Var_2, Var_3))
is
Var_2 : Integer;
Var_3 : Integer;
procedure In_Out_Proc_1
with Refined_Global => (In_Out => Var_1) -- OK
is begin null; end In_Out_Proc_1;
procedure In_Out_Proc_2
with Refined_Global => (Input => Var_1, -- OK
Output => Var_2) -- OK
is begin null; end In_Out_Proc_2;
procedure In_Out_Proc_3
with Refined_Global => (Output => Var_3) -- OK
is begin null; end In_Out_Proc_3;
procedure In_Out_Proc_4
with Refined_Global => (Input => (Var_1)) -- illegal
is begin null; end In_Out_Proc_4;
procedure In_Out_Proc_5
with Refined_Global => (Output => (Var_1, Var_2, Var_3)) -- illegal
is begin null; end In_Out_Proc_5;
end In_Out_State_Checks;
package body Output_State_Checks
with Refined_State => (Output_State => (Var_1, Var_2, Var_3))
is
Var_2 : Integer;
Var_3 : Integer;
procedure Output_Proc_1
with Refined_Global => (Output => (Var_1, Var_3)) -- illegal
is begin null; end Output_Proc_1;
procedure Output_Proc_2
with Refined_Global => (Input => Var_1, -- illegal
Output => (Var_2, Var_3)) -- OK
is begin null; end Output_Proc_2;
end Output_State_Checks;
end Completions;
-- inconsistencies.ads
package Inconsistencies
with Abstract_State => State
is
Var_1 : Integer;
Var_2 : Integer;
Extra : Integer;
procedure Mismatched_Items
with Global => (Input => Var_1,
In_Out => State,
Output => Var_2);
private
Var_3 : Integer;
end Inconsistencies;
-- inconsistencies.adb
package body Inconsistencies
with Refined_State => (State => (Var_3, Var_4))
is
Var_4 : Integer;
procedure Mismatched_Items
with Refined_Global => (Input => Var_2,
In_Out => (Var_4, Extra),
Output => Var_1)
is begin null; end Mismatched_Items;
end Inconsistencies;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnat12 -gnatd.V -gnatws semantics.adb
$ gcc -c -gnat12 -gnatd.V completions.adb
$ gcc -c -gnat12 -gnatd.V inconsistencies.adb
completions.adb:9:14: constituent "Var_2" of state "Input_State" must have mode
Input in global refinement
completions.adb:34:14: global refinement of state "In_Out_State" redefines the
mode of its constituents
completions.adb:38:14: global refinement of state "In_Out_State" redefines the
mode of its constituents
completions.adb:49:14: constituent "Var_2" of state "Output_State" must have
mode Output in global refinement
completions.adb:53:14: constituent "Var_1" of state "Output_State" must have
mode Output in global refinement
inconsistencies.adb:7:40: global item "Var_2" has inconsistent modes
inconsistencies.adb:7:40: expected mode "Input"
inconsistencies.adb:7:40: found mode "Output"
inconsistencies.adb:8:48: extra global item "Extra"
inconsistencies.adb:9:40: global item "Var_1" has inconsistent modes
inconsistencies.adb:9:40: expected mode "Output"
inconsistencies.adb:9:40: found mode "Input"
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-10-13 Hristian Kirtchev <kirtchev@adacore.com>
* einfo.adb: Add node/list usage for Refined_State
and Refinement_Constituents.
(Get_Pragma): Update the
initialization of Is_CDG to include Refined_Global and
Refined_Depends. Rename constant Delayed to In_Contract and update
all of its occurrences.
(Is_Non_Volatile_State): New routine.
(Is_Volatile_State): Removed.
(Refined_State): New routine.
(Refinement_Constituents): New routine.
(Set_Refined_State): New routine.
(Set_Refinement_Constituents): New routine.
(Write_Field8_Name): Add output for Refinement_Constituents.
(Write_Field10_Name): Add output for Refined_State.
* einfo.ads: Add new synthesized attribute Is_Non_Volatile_State.
Remove synthesized attribute Is_Volatile_State. Add new
attributes Refined_State and Refinement_Constituents along with
usage in nodes.
(Get_Pragma): Update the comment on usage.
(Is_Non_Volatile_State): New routine.
(Is_Volatile_State): Removed.
(Refined_State): New routine and pragma Inline.
(Refinement_Constituents): New routine and pragma Inline.
(Set_Refined_State): New routine and pragma Inline.
(Set_Refinement_Constituents): New routine and pragma Inline.
* elists.ads, elists.adb (Clone): Removed.
(New_Copy_Elist): New routine.
(Remove): New routine.
* sem_ch3.adb (Analyze_Declarations): Use Defining_Entity
to get the entity of the subprogram [body].
(Analyze_Object_Declaration): Add initialization for
Refined_State.
* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add processing
for Refined_Global and Refined_Depends. Emit an error when
the body requires Refined_Global, but the aspect/pragma is
not present.
* sem_ch6.ads (Analyze_Subprogram_Body_Contract): Change
procedure signature and add comment on usage.
* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
for aspect Refined_Global.
* sem_prag.adb (Analyze_Abstract_State): Add initialization
of attributes Refined_State and Refinement_Constituents.
(Analyze_Depends_In_Decl_Part, Analyze_Global_In_Decl_Part,
Analyze_Contract_Cases_In_Decl_Part): Remove local
constant Arg1.
(Analyze_Pragma): Add processing for pragma
Refined_Global. The analysis of Refined_Post and Refined_Pre
has been merged. Update an error message in the processing of
pragma Refined_State.
(Analyze_Refined_Global_In_Decl_Part): Provide implementation.
(Analyze_Refined_Pragma): New routine.
(Analyze_Refined_Pre_Post_Condition): Removed.
(Analyze_Refined_State_In_Decl_Part): Update the call to Clone.
(Analyze_Refinement_Clause): Make State_Id visible to all
nested subprogram.
(Check_Matching_Constituent): Establish
a relation between a refined state and its constituent.
(Collect_Hidden_States_In_Decls): Remove ??? comment. Look at
the entity of the object declaration to establish its kind.
* sem_util.adb: Alphabetize with and use clauses.
(Contains_Refined_State): New routine.
* sem_util.ads (Contains_Refined_State): New routine.
-------------- next part --------------
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 203503)
+++ sem_ch3.adb (revision 203504)
@@ -2233,12 +2233,10 @@
Decl := First (L);
while Present (Decl) loop
if Nkind (Decl) = N_Subprogram_Body then
- Analyze_Subprogram_Body_Contract
- (Defining_Unit_Name (Specification (Decl)));
+ Analyze_Subprogram_Body_Contract (Defining_Entity (Decl));
elsif Nkind (Decl) = N_Subprogram_Declaration then
- Analyze_Subprogram_Contract
- (Defining_Unit_Name (Specification (Decl)));
+ Analyze_Subprogram_Contract (Defining_Entity (Decl));
end if;
Next (Decl);
@@ -3540,7 +3538,7 @@
if Constant_Present (N) then
Set_Ekind (Id, E_Constant);
- Set_Is_True_Constant (Id, True);
+ Set_Is_True_Constant (Id);
else
Set_Ekind (Id, E_Variable);
@@ -3763,6 +3761,13 @@
end if;
<<Leave>>
+ -- Initialize the refined state of a variable here because this is a
+ -- common destination for legal and illegal object declarations.
+
+ if Ekind (Id) = E_Variable then
+ Set_Refined_State (Id, Empty);
+ end if;
+
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
Index: einfo.adb
===================================================================
--- einfo.adb (revision 203503)
+++ einfo.adb (revision 203504)
@@ -81,6 +81,7 @@
-- Normalized_First_Bit Uint8
-- Postcondition_Proc Node8
-- Refined_State_Pragma Node8
+ -- Refinement_Constituents Elist8
-- Return_Applies_To Node8
-- First_Exit_Statement Node8
@@ -93,6 +94,7 @@
-- Float_Rep Uint10 (but returns Float_Rep_Kind)
-- Handler_Records List10
-- Normalized_Position_Max Uint10
+ -- Refined_State Node10
-- Component_Bit_Offset Uint11
-- Full_View Node11
@@ -2648,12 +2650,24 @@
return Flag227 (Id);
end Referenced_As_Out_Parameter;
+ function Refined_State (Id : E) return N is
+ begin
+ pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
+ return Node10 (Id);
+ end Refined_State;
+
function Refined_State_Pragma (Id : E) return N is
begin
pragma Assert (Ekind (Id) = E_Package_Body);
return Node8 (Id);
end Refined_State_Pragma;
+ function Refinement_Constituents (Id : E) return L is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ return Elist8 (Id);
+ end Refinement_Constituents;
+
function Register_Exception_Call (Id : E) return N is
begin
pragma Assert (Ekind (Id) = E_Exception);
@@ -5308,12 +5322,24 @@
Set_Flag227 (Id, V);
end Set_Referenced_As_Out_Parameter;
+ procedure Set_Refined_State (Id : E; V : E) is
+ begin
+ pragma Assert (Ekind_In (Id, E_Abstract_State, E_Variable));
+ Set_Node10 (Id, V);
+ end Set_Refined_State;
+
procedure Set_Refined_State_Pragma (Id : E; V : N) is
begin
pragma Assert (Ekind (Id) = E_Package_Body);
Set_Node8 (Id, V);
end Set_Refined_State_Pragma;
+ procedure Set_Refinement_Constituents (Id : E; V : L) is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ Set_Elist8 (Id, V);
+ end Set_Refinement_Constituents;
+
procedure Set_Register_Exception_Call (Id : E; V : N) is
begin
pragma Assert (Ekind (Id) = E_Exception);
@@ -6266,21 +6292,26 @@
----------------
function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is
- Is_CDG : constant Boolean :=
- Id = Pragma_Depends or else Id = Pragma_Global;
- Is_CTC : constant Boolean :=
- Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case;
- Is_PPC : constant Boolean :=
- Id = Pragma_Precondition or else Id = Pragma_Postcondition;
- Delayed : constant Boolean := Is_CDG or Is_CTC or Is_PPC;
- Item : Node_Id;
- Items : Node_Id;
+ Is_CDG : constant Boolean :=
+ Id = Pragma_Depends
+ or else Id = Pragma_Global
+ or else Id = Pragma_Refined_Depends
+ or else Id = Pragma_Refined_Global;
+ Is_CTC : constant Boolean :=
+ Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case;
+ Is_PPC : constant Boolean :=
+ Id = Pragma_Precondition
+ or else Id = Pragma_Postcondition;
+ In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC;
+ Item : Node_Id;
+ Items : Node_Id;
+
begin
- -- Handle delayed pragmas that appear in N_Contract nodes. Those have to
- -- be extracted from their specialized list.
+ -- Handle pragmas that appear in N_Contract nodes. Those have to be
+ -- extracted from their specialized list.
- if Delayed then
+ if In_Contract then
Items := Contract (E);
if No (Items) then
@@ -6310,7 +6341,7 @@
-- All nodes in N_Contract are chained using Next_Pragma
- elsif Delayed then
+ elsif In_Contract then
Item := Next_Pragma (Item);
-- Regular pragmas
@@ -6712,6 +6743,17 @@
and then Has_Option (Id, Name_Input_Only);
end Is_Input_Only_State;
+ ---------------------------
+ -- Is_Non_Volatile_State --
+ ---------------------------
+
+ function Is_Non_Volatile_State (Id : E) return B is
+ begin
+ return
+ Ekind (Id) = E_Abstract_State
+ and then Has_Option (Id, Name_Non_Volatile);
+ end Is_Non_Volatile_State;
+
-------------------
-- Is_Null_State --
-------------------
@@ -6872,17 +6914,6 @@
and then Is_Task_Type (Corresponding_Concurrent_Type (Id));
end Is_Task_Record_Type;
- -----------------------
- -- Is_Volatile_State --
- -----------------------
-
- function Is_Volatile_State (Id : E) return B is
- begin
- return
- Ekind (Id) = E_Abstract_State
- and then Has_Option (Id, Name_Volatile);
- end Is_Volatile_State;
-
------------------------
-- Is_Wrapper_Package --
------------------------
@@ -8309,6 +8340,9 @@
when E_Package_Body =>
Write_Str ("Refined_State_Pragma");
+ when E_Abstract_State =>
+ Write_Str ("Refinement_Constituents");
+
when E_Return_Statement =>
Write_Str ("Return_Applies_To");
@@ -8358,7 +8392,7 @@
Concurrent_Kind =>
Write_Str ("Direct_Primitive_Operations");
- when Float_Kind =>
+ when Float_Kind =>
Write_Str ("Float_Rep");
when E_In_Parameter |
@@ -8375,6 +8409,10 @@
E_Discriminant =>
Write_Str ("Normalized_Position_Max");
+ when E_Abstract_State |
+ E_Variable =>
+ Write_Str ("Refined_State");
+
when others =>
Write_Str ("Field10??");
end case;
Index: einfo.ads
===================================================================
--- einfo.ads (revision 203503)
+++ einfo.ads (revision 203504)
@@ -2576,6 +2576,10 @@
-- set right, at which point, these comments can be removed, and the
-- tests for static subtypes greatly simplified.
+-- Is_Non_Volatile_State (synthesized)
+-- Applies to all entities, true for abstract states that are subject to
+-- option Non_Volatile.
+
-- Is_Null_Init_Proc (Flag178)
-- Defined in procedure entities. Set for generated init proc procedures
-- (used to initialize composite types), if the code for the procedure
@@ -2977,10 +2981,6 @@
-- optimizations on volatile objects should test Treat_As_Volatile
-- rather than testing this flag.
--- Is_Volatile_State (synthesized)
--- Applies to all entities, true for abstract states that are subject to
--- option Volatile.
-
-- Is_Wrapper_Package (synthesized)
-- Defined in package entities. Indicates that the package has been
-- created as a wrapper for a subprogram instantiation.
@@ -3537,10 +3537,19 @@
-- we have a separate warning for variables that are only assigned and
-- never read, and out parameters are a special case.
+-- Refined_State (Node10)
+-- Defined in abstract states and variables. Contains the entity of an
+-- ancestor state whose refinement mentions this item.
+
-- Refined_State_Pragma (Node8)
-- Defined in [generic] package bodies. Contains the pragma that refines
-- all abstract states defined in the corresponding package declaration.
+-- Refinement_Constituents (Elist8)
+-- Present in abstract state entities. Contains all the constituents that
+-- refine the state, in other words, all the hidden states that appear in
+-- the constituent_list of aspect/pragma Refined_State.
+
-- Register_Exception_Call (Node20)
-- Defined in exception entities. When an exception is declared,
-- a call is expanded to Register_Exception. This field points to
@@ -5096,11 +5105,13 @@
------------------------------------------
-- E_Abstract_State
+ -- Refinement_Constituents (Elist8)
+ -- Refined_State (Node10)
-- Is_External_State (synth)
-- Is_Input_Only_State (synth)
-- Is_Null_State (synth)
-- Is_Output_Only_State (synth)
- -- Is_Volatile_State (synth)
+ -- Is_Non_Volatile_State (synth)
-- E_Access_Protected_Subprogram_Type
-- Equivalent_Type (Node18)
@@ -5913,6 +5924,7 @@
-- E_Variable
-- Hiding_Loop_Variable (Node8)
-- Current_Value (Node9)
+ -- Refined_State (Node10)
-- Esize (Uint12)
-- Extra_Accessibility (Node13)
-- Alignment (Uint14)
@@ -6540,7 +6552,9 @@
function Referenced (Id : E) return B;
function Referenced_As_LHS (Id : E) return B;
function Referenced_As_Out_Parameter (Id : E) return B;
+ function Refined_State (Id : E) return E;
function Refined_State_Pragma (Id : E) return E;
+ function Refinement_Constituents (Id : E) return L;
function Register_Exception_Call (Id : E) return N;
function Related_Array_Object (Id : E) return E;
function Related_Expression (Id : E) return N;
@@ -6691,6 +6705,7 @@
function Is_Ghost_Entity (Id : E) return B;
function Is_Ghost_Subprogram (Id : E) return B;
function Is_Input_Only_State (Id : E) return B;
+ function Is_Non_Volatile_State (Id : E) return B;
function Is_Null_State (Id : E) return B;
function Is_Output_Only_State (Id : E) return B;
function Is_Package_Or_Generic_Package (Id : E) return B;
@@ -6703,7 +6718,6 @@
function Is_Synchronized_Interface (Id : E) return B;
function Is_Task_Interface (Id : E) return B;
function Is_Task_Record_Type (Id : E) return B;
- function Is_Volatile_State (Id : E) return B;
function Is_Wrapper_Package (Id : E) return B;
function Last_Formal (Id : E) return E;
function Machine_Emax_Value (Id : E) return U;
@@ -7158,7 +7172,9 @@
procedure Set_Referenced (Id : E; V : B := True);
procedure Set_Referenced_As_LHS (Id : E; V : B := True);
procedure Set_Referenced_As_Out_Parameter (Id : E; V : B := True);
+ procedure Set_Refined_State (Id : E; V : E);
procedure Set_Refined_State_Pragma (Id : E; V : N);
+ procedure Set_Refinement_Constituents (Id : E; V : L);
procedure Set_Register_Exception_Call (Id : E; V : N);
procedure Set_Related_Array_Object (Id : E; V : E);
procedure Set_Related_Expression (Id : E; V : N);
@@ -7403,11 +7419,17 @@
-- Empty is returned.
function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id;
- -- Searches the Rep_Item chain for a given entity E, for an instance of
- -- a pragma with the given pragma Id. If found, the value returned is the
- -- N_Pragma node, otherwise Empty is returned. Delayed pragmas such as
- -- Precondition, Postcondition, Contract_Cases, Depends and Global appear
- -- in the N_Contract node of entity E and are also handled by this routine.
+ -- Searches the Rep_Item chain of entity E, for an instance of a pragma
+ -- with the given pragma Id. If found, the value returned is the N_Pragma
+ -- node, otherwise Empty is returned. The following contract pragmas that
+ -- appear in N_Contract nodes are also handled by this routine:
+ -- Contract_Cases
+ -- Depends
+ -- Global
+ -- Precondition
+ -- Postcondition
+ -- Refined_Depends
+ -- Refined_Global
function Get_Record_Representation_Clause (E : Entity_Id) return Node_Id;
-- Searches the Rep_Item chain for a given entity E, for a record
@@ -7908,7 +7930,9 @@
pragma Inline (Referenced);
pragma Inline (Referenced_As_LHS);
pragma Inline (Referenced_As_Out_Parameter);
+ pragma Inline (Refined_State);
pragma Inline (Refined_State_Pragma);
+ pragma Inline (Refinement_Constituents);
pragma Inline (Register_Exception_Call);
pragma Inline (Related_Array_Object);
pragma Inline (Related_Expression);
@@ -8324,7 +8348,9 @@
pragma Inline (Set_Referenced);
pragma Inline (Set_Referenced_As_LHS);
pragma Inline (Set_Referenced_As_Out_Parameter);
+ pragma Inline (Set_Refined_State);
pragma Inline (Set_Refined_State_Pragma);
+ pragma Inline (Set_Refinement_Constituents);
pragma Inline (Set_Register_Exception_Call);
pragma Inline (Set_Related_Array_Object);
pragma Inline (Set_Related_Expression);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 203503)
+++ sem_prag.adb (revision 203504)
@@ -401,7 +401,6 @@
-- Local variables
- Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
All_Cases : Node_Id;
CCase : Node_Id;
Subp_Decl : Node_Id;
@@ -417,7 +416,7 @@
Subp_Decl := Find_Related_Subprogram (N);
Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
- All_Cases := Expression (Arg1);
+ All_Cases := Expression (First (Pragma_Argument_Associations (N)));
-- Multiple contract cases appear in aggregate form
@@ -460,8 +459,7 @@
----------------------------------
procedure Analyze_Depends_In_Decl_Part (N : Node_Id) is
- Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
- Loc : constant Source_Ptr := Sloc (N);
+ Loc : constant Source_Ptr := Sloc (N);
All_Inputs_Seen : Elist_Id := No_Elist;
-- A list containing the entities of all the inputs processed so far.
@@ -1248,7 +1246,7 @@
Subp_Decl := Find_Related_Subprogram (N);
Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
- Clause := Expression (Arg1);
+ Clause := Expression (First (Pragma_Argument_Associations (N)));
-- Empty dependency list
@@ -1348,8 +1346,6 @@
---------------------------------
procedure Analyze_Global_In_Decl_Part (N : Node_Id) is
- Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
-
Seen : Elist_Id := No_Elist;
-- A list containing the entities of all the items processed so far. It
-- plays a role in detecting distinct entities.
@@ -1680,7 +1676,7 @@
Next (Assoc);
end loop;
- -- Something went horribly wrong, we have a malformed tree
+ -- Invalid tree
else
raise Program_Error;
@@ -1708,7 +1704,7 @@
Subp_Decl := Find_Related_Subprogram (N);
Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
- List := Expression (Arg1);
+ List := Expression (First (Pragma_Argument_Associations (N)));
-- There is nothing to be done for a null global list
@@ -1781,9 +1777,15 @@
-- In Ada 95 or 05 mode, these are implementation defined pragmas, so
-- should be caught by the No_Implementation_Pragmas restriction.
- procedure Analyze_Refined_Pre_Post_Condition;
- -- Subsidiary routine to the analysis of pragmas Refined_Pre and
- -- Refined_Post.
+ procedure Analyze_Refined_Pragma
+ (Spec_Id : out Entity_Id;
+ Body_Id : out Entity_Id;
+ Legal : out Boolean);
+ -- Subsidiary routine to the analysis of body pragmas Refined_Depends,
+ -- Refined_Global, Refined_Post and Refined_Pre. Check the placement and
+ -- related context of the pragma. Spec_Id is the entity of the related
+ -- subprogram. Body_Id is the entity of the subprogram body. Flag Legal
+ -- is set when the pragma is properly placed.
procedure Check_Ada_83_Warning;
-- Issues a warning message for the current pragma if operating in Ada
@@ -2311,18 +2313,27 @@
end if;
end Ada_2012_Pragma;
- ----------------------------------------
- -- Analyze_Refined_Pre_Post_Condition --
- ----------------------------------------
+ ----------------------------
+ -- Analyze_Refined_Pragma --
+ ----------------------------
- procedure Analyze_Refined_Pre_Post_Condition is
+ procedure Analyze_Refined_Pragma
+ (Spec_Id : out Entity_Id;
+ Body_Id : out Entity_Id;
+ Legal : out Boolean)
+ is
Body_Decl : Node_Id := Parent (N);
Pack_Spec : Node_Id;
Spec_Decl : Node_Id;
- Spec_Id : Entity_Id;
Stmt : Node_Id;
begin
+ -- Assume that the pragma is illegal
+
+ Spec_Id := Empty;
+ Body_Id := Empty;
+ Legal := False;
+
GNAT_Pragma;
Check_Arg_Count (1);
Check_No_Identifiers;
@@ -2385,6 +2396,8 @@
return;
end if;
+ Body_Id := Defining_Entity (Body_Decl);
+
-- The body [stub] must not act as a spec, in other words it has to
-- be paired with a corresponding spec.
@@ -2421,10 +2434,10 @@
return;
end if;
- -- Analyze the boolean expression as a "spec expression"
+ -- If we get here, then the pragma is legal
- Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id);
- end Analyze_Refined_Pre_Post_Condition;
+ Legal := True;
+ end Analyze_Refined_Pragma;
--------------------------
-- Check_Ada_83_Warning --
@@ -8492,10 +8505,12 @@
-- from the original state declaration. Decorate the entity.
Id := Make_Defining_Identifier (Loc, New_External_Name (Name));
- Set_Comes_From_Source (Id, not Is_Null);
- Set_Parent (Id, State);
- Set_Ekind (Id, E_Abstract_State);
- Set_Etype (Id, Standard_Void_Type);
+ Set_Comes_From_Source (Id, not Is_Null);
+ Set_Parent (Id, State);
+ Set_Ekind (Id, E_Abstract_State);
+ Set_Etype (Id, Standard_Void_Type);
+ Set_Refined_State (Id, Empty);
+ Set_Refinement_Constituents (Id, New_Elmt_List);
-- Every non-null state must be nameable and resolvable the
-- same way a constant is.
@@ -11873,7 +11888,7 @@
-- Global --
------------
- -- pragma Global (GLOBAL_SPECIFICATION)
+ -- pragma Global (GLOBAL_SPECIFICATION);
-- GLOBAL_SPECIFICATION ::=
-- null
@@ -15939,31 +15954,59 @@
-- Refined_Global --
--------------------
- -- ??? To be implemented
+ -- pragma Refined_Global (GLOBAL_SPECIFICATION);
- -- Would be better if these generated an error message saying that
- -- the feature was not yet implemented ???
+ -- GLOBAL_SPECIFICATION ::=
+ -- null
+ -- | GLOBAL_LIST
+ -- | MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST}
- when Pragma_Refined_Global =>
- null;
+ -- MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST
- ------------------
- -- Refined_Post --
- ------------------
+ -- MODE_SELECTOR ::= Input | Output | In_Out | Contract_In
+ -- GLOBAL_LIST ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM})
+ -- GLOBAL_ITEM ::= NAME
+ when Pragma_Refined_Global => Refined_Global : declare
+ Body_Id : Entity_Id;
+ Legal : Boolean;
+ Spec_Id : Entity_Id;
+
+ begin
+ Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal);
+
+ -- Save the pragma in the contract of the subprogram body. The
+ -- remaining analysis is performed at the end of the enclosing
+ -- declarations.
+
+ if Legal then
+ Add_Contract_Item (N, Body_Id);
+ end if;
+ end Refined_Global;
+
+ ------------------------------
+ -- Refined_Post/Refined_Pre --
+ ------------------------------
+
-- pragma Refined_Post (boolean_EXPRESSION);
+ -- pragma Refined_Pre (boolean_EXPRESSION);
- when Pragma_Refined_Post =>
- Analyze_Refined_Pre_Post_Condition;
+ when Pragma_Refined_Post |
+ Pragma_Refined_Pre => Refined_Pre_Post :
+ declare
+ Body_Id : Entity_Id;
+ Legal : Boolean;
+ Spec_Id : Entity_Id;
- -----------------
- -- Refined_Pre --
- -----------------
+ begin
+ Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal);
- -- pragma Refined_Pre (boolean_EXPRESSION);
+ -- Analyze the boolean expression as a "spec expression"
- when Pragma_Refined_Pre =>
- Analyze_Refined_Pre_Post_Condition;
+ if Legal then
+ Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id);
+ end if;
+ end Refined_Pre_Post;
-------------------
-- Refined_State --
@@ -16009,8 +16052,9 @@
if No (Abstract_States (Spec_Id))
or else Has_Null_Abstract_State (Spec_Id)
then
- Error_Pragma
- ("useless pragma %, package does not define abstract states");
+ Error_Msg_NE
+ ("useless refinement, package & does not define abstract "
+ & "states", N, Spec_Id);
return;
end if;
@@ -18534,12 +18578,874 @@
-- Analyze_Refined_Global_In_Decl_Part --
-----------------------------------------
- -- ??? To be implemented
+ procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id) is
+ Global : Node_Id;
+ -- The corresponding Global aspect/pragma
- procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id) is
- pragma Unreferenced (N);
+ Has_In_State : Boolean := False;
+ Has_In_Out_State : Boolean := False;
+ Has_Out_State : Boolean := False;
+ -- These flags are set when the corresponding Global aspect/pragma has
+ -- a state of mode Input, In_Out and Output respectively with a visible
+ -- refinement.
+
+ In_Constits : Elist_Id := No_Elist;
+ In_Out_Constits : Elist_Id := No_Elist;
+ Out_Constits : Elist_Id := No_Elist;
+ -- These lists contain the entities of all Input, In_Out and Output
+ -- constituents that appear in Refined_Global and participate in state
+ -- refinement.
+
+ In_Items : Elist_Id := No_Elist;
+ In_Out_Items : Elist_Id := No_Elist;
+ Out_Items : Elist_Id := No_Elist;
+ -- These list contain the entities of all Input, In_Out and Output items
+ -- defined in the corresponding Global aspect.
+
+ procedure Check_In_Out_States;
+ -- Determine whether the corresponding Global aspect/pragma mentions
+ -- In_Out states with visible refinement and if so, ensure that one of
+ -- the following completions apply to the constituents of the state:
+ -- 1) there is at least one constituent of mode In_Out
+ -- 2) there is at least one Input and one Output constituent
+ -- 3) not all constituents are present and one of them is of mode
+ -- Output.
+ -- This routine may remove elements from In_Constits, In_Out_Constits
+ -- and Out_Constits.
+
+ procedure Check_Input_States;
+ -- Determine whether the corresponding Global aspect/pragma mentions
+ -- Input states with visible refinement and if so, ensure that at least
+ -- one of its constituents appears as an Input item in Refined_Global.
+ -- This routine may remove elements from In_Constits, In_Out_Constits
+ -- and Out_Constits.
+
+ procedure Check_Output_States;
+ -- Determine whether the corresponding Global aspect/pragma mentions
+ -- Output states with visible refinement and if so, ensure that all of
+ -- its constituents appear as Output items in Refined_Global. This
+ -- routine may remove elements from In_Constits, In_Out_Constits and
+ -- Out_Constits.
+
+ procedure Check_Refined_Global_List
+ (List : Node_Id;
+ Global_Mode : Name_Id := Name_Input);
+ -- Verify the legality of a single global list declaration. Global_Mode
+ -- denotes the current mode in effect.
+
+ procedure Collect_Global_Items (Prag : Node_Id);
+ -- Collect the entities of all items of pragma Prag by populating lists
+ -- In_Items, In_Out_Items and Out_Items. The routine also sets flags
+ -- Has_In_State, Has_In_Out_State and Has_Out_State if there is a state
+ -- of a particular kind with visible refinement.
+
+ function Present_Then_Remove
+ (List : Elist_Id;
+ Item : Entity_Id) return Boolean;
+ -- Search List for a particular entity Item. If Item has been found,
+ -- remove it from List. This routine is used to strip lists In_Constits,
+ -- In_Out_Constits and Out_Constits of valid constituents.
+
+ procedure Report_Extra_Constituents;
+ -- Emit an error for each constituent found in lists In_Constits,
+ -- In_Out_Constits and Out_Constits.
+
+ -------------------------
+ -- Check_In_Out_States --
+ -------------------------
+
+ procedure Check_In_Out_States is
+ procedure Check_Constituent_Usage (State_Id : Entity_Id);
+ -- Determine whether one of the following coverage scenarios is in
+ -- effect:
+ -- 1) there is at least one constituent of mode In_Out
+ -- 2) there is at least one Input and one Output constituent
+ -- 3) not all constituents are present and one of them is of mode
+ -- Output.
+ -- If this is not the case, emit an error.
+
+ -----------------------------
+ -- Check_Constituent_Usage --
+ -----------------------------
+
+ procedure Check_Constituent_Usage (State_Id : Entity_Id) is
+ Constit_Elmt : Elmt_Id;
+ Constit_Id : Entity_Id;
+ Has_Missing : Boolean := False;
+ In_Out_Seen : Boolean := False;
+ In_Seen : Boolean := False;
+ Out_Seen : Boolean := False;
+
+ begin
+ -- 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_Then_Remove (In_Constits, Constit_Id) then
+ In_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
+ Out_Seen := True;
+
+ else
+ Has_Missing := True;
+ end if;
+
+ Next_Elmt (Constit_Elmt);
+ end loop;
+
+ -- A single In_Out constituent is a valid completion
+
+ if In_Out_Seen then
+ null;
+
+ -- A pair of one Input and one Output constituent is a valid
+ -- completion.
+
+ elsif In_Seen and then Out_Seen then
+ null;
+
+ -- A single Output constituent is a valid completion only when
+ -- some of the other constituents are missing.
+
+ elsif Has_Missing and then Out_Seen then
+ null;
+
+ else
+ Error_Msg_NE
+ ("global refinement of state & redefines the mode of its "
+ & "constituents", N, State_Id);
+ end if;
+ end Check_Constituent_Usage;
+
+ -- Local variables
+
+ Item_Elmt : Elmt_Id;
+ Item_Id : Entity_Id;
+
+ -- Start of processing for Check_In_Out_States
+
+ begin
+ -- Inspect the In_Out items of the corresponding Global aspect/pragma
+ -- looking for a state with a visible refinement.
+
+ if Has_In_Out_State and then Present (In_Out_Items) then
+ Item_Elmt := First_Elmt (In_Out_Items);
+ while Present (Item_Elmt) loop
+ Item_Id := Node (Item_Elmt);
+
+ -- Ensure that one of the three coverage variants is satisfied
+
+ if Ekind (Item_Id) = E_Abstract_State
+ and then Present (Refinement_Constituents (Item_Id))
+ then
+ Check_Constituent_Usage (Item_Id);
+ end if;
+
+ Next_Elmt (Item_Elmt);
+ end loop;
+ end if;
+ end Check_In_Out_States;
+
+ ------------------------
+ -- Check_Input_States --
+ ------------------------
+
+ procedure Check_Input_States is
+ procedure Check_Constituent_Usage (State_Id : Entity_Id);
+ -- Determine whether at least one constituent of state State_Id with
+ -- visible refinement is used and has mode Input. Ensure that the
+ -- remaining constituents do not have In_Out or Output modes.
+
+ -----------------------------
+ -- Check_Constituent_Usage --
+ -----------------------------
+
+ procedure Check_Constituent_Usage (State_Id : Entity_Id) is
+ 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);
+
+ -- At least one of the constituents appears as an Input
+
+ if Present_Then_Remove (In_Constits, Constit_Id) then
+ In_Seen := True;
+
+ -- The constituent appears in the global refinement, but has
+ -- mode In_Out or Output.
+
+ 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);
+ Error_Msg_NE
+ ("constituent & of state % must have mode Input in global "
+ & "refinement", N, Constit_Id);
+ end if;
+
+ Next_Elmt (Constit_Elmt);
+ end loop;
+
+ -- Not one of the constituents appeared as Input
+
+ if not In_Seen then
+ Error_Msg_NE
+ ("global refinement of state & must include at least one "
+ & "constituent of mode Input", N, State_Id);
+ end if;
+ end Check_Constituent_Usage;
+
+ -- Local variables
+
+ Item_Elmt : Elmt_Id;
+ Item_Id : Entity_Id;
+
+ -- Start of processing for Check_Input_States
+
+ begin
+ -- Inspect the Input items of the corresponding Global aspect/pragma
+ -- looking for a state with a visible refinement.
+
+ if Has_In_State and then Present (In_Items) then
+ Item_Elmt := First_Elmt (In_Items);
+ while Present (Item_Elmt) loop
+ Item_Id := Node (Item_Elmt);
+
+ -- Ensure that at least one of the constituents is utilized and
+ -- is of mode Input.
+
+ if Ekind (Item_Id) = E_Abstract_State
+ and then Present (Refinement_Constituents (Item_Id))
+ then
+ Check_Constituent_Usage (Item_Id);
+ end if;
+
+ Next_Elmt (Item_Elmt);
+ end loop;
+ end if;
+ end Check_Input_States;
+
+ -------------------------
+ -- Check_Output_States --
+ -------------------------
+
+ procedure Check_Output_States is
+ procedure Check_Constituent_Usage (State_Id : Entity_Id);
+ -- Determine whether all constituents of state State_Id with visible
+ -- refinement are used and have mode Output. Emit an error if this is
+ -- not the case.
+
+ -----------------------------
+ -- Check_Constituent_Usage --
+ -----------------------------
+
+ procedure Check_Constituent_Usage (State_Id : Entity_Id) is
+ Constit_Elmt : Elmt_Id;
+ Constit_Id : Entity_Id;
+
+ begin
+ Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id));
+ while Present (Constit_Elmt) loop
+ Constit_Id := Node (Constit_Elmt);
+
+ if Present_Then_Remove (Out_Constits, Constit_Id) then
+ null;
+
+ else
+ Remove (In_Constits, Constit_Id);
+ Remove (In_Out_Constits, Constit_Id);
+
+ Error_Msg_Name_1 := Chars (State_Id);
+ Error_Msg_NE
+ ("constituent & of state % must have mode Output in "
+ & "global refinement", N, Constit_Id);
+ end if;
+
+ Next_Elmt (Constit_Elmt);
+ end loop;
+ end Check_Constituent_Usage;
+
+ -- Local variables
+
+ Item_Elmt : Elmt_Id;
+ Item_Id : Entity_Id;
+
+ -- Start of processing for Check_Output_States
+
+ begin
+ -- Inspect the Output items of the corresponding Global aspect/pragma
+ -- looking for a state with a visible refinement.
+
+ if Has_Out_State and then Present (Out_Items) then
+ Item_Elmt := First_Elmt (Out_Items);
+ while Present (Item_Elmt) loop
+ Item_Id := Node (Item_Elmt);
+
+ -- Ensure that all of the constituents are utilized and they
+ -- have mode Output.
+
+ if Ekind (Item_Id) = E_Abstract_State
+ and then Present (Refinement_Constituents (Item_Id))
+ then
+ Check_Constituent_Usage (Item_Id);
+ end if;
+
+ Next_Elmt (Item_Elmt);
+ end loop;
+ end if;
+ end Check_Output_States;
+
+ -------------------------------
+ -- Check_Refined_Global_List --
+ -------------------------------
+
+ procedure Check_Refined_Global_List
+ (List : Node_Id;
+ Global_Mode : Name_Id := Name_Input)
+ is
+ procedure Check_Refined_Global_Item
+ (Item : Node_Id;
+ Global_Mode : Name_Id);
+ -- Verify the legality of a single global item declaration. Parameter
+ -- Global_Mode denotes the current mode in effect.
+
+ -------------------------------
+ -- Check_Refined_Global_Item --
+ -------------------------------
+
+ procedure Check_Refined_Global_Item
+ (Item : Node_Id;
+ Global_Mode : Name_Id)
+ is
+ procedure Add_Constituent (Item_Id : Entity_Id);
+ -- Add a single constituent to one of the three constituent lists
+ -- depending on Global_Mode.
+
+ procedure Check_Matching_Modes (Item_Id : Entity_Id);
+ -- Verify that the global modes of item Item_Id are the same in
+ -- both aspects/pragmas Global and Refined_Global.
+
+ function Is_Part_Of
+ (State : Entity_Id;
+ Ancestor : Entity_Id) return Boolean;
+ -- Determine whether abstract state State is part of an ancestor
+ -- abstract state Ancestor. For this relationship to hold, State
+ -- must have option Part_Of in its Abstract_State definition.
+
+ ---------------------
+ -- Add_Constituent --
+ ---------------------
+
+ procedure Add_Constituent (Item_Id : Entity_Id) is
+ begin
+ if Global_Mode = Name_Input then
+ Add_Item (Item_Id, In_Constits);
+
+ elsif Global_Mode = Name_In_Out then
+ Add_Item (Item_Id, In_Out_Constits);
+
+ elsif Global_Mode = Name_Output then
+ Add_Item (Item_Id, Out_Constits);
+ end if;
+ end Add_Constituent;
+
+ --------------------------
+ -- Check_Matching_Modes --
+ --------------------------
+
+ procedure Check_Matching_Modes (Item_Id : Entity_Id) is
+ procedure Inconsistent_Mode_Error (Expect : Name_Id);
+ -- Issue a common error message for all mode mismatche. Expect
+ -- denotes the expected mode.
+
+ -----------------------------
+ -- Inconsistent_Mode_Error --
+ -----------------------------
+
+ procedure Inconsistent_Mode_Error (Expect : Name_Id) is
+ begin
+ Error_Msg_NE
+ ("global item & has inconsistent modes", Item, Item_Id);
+
+ Error_Msg_Name_1 := Global_Mode;
+ Error_Msg_N ("\ expected mode %", Item);
+
+ Error_Msg_Name_1 := Expect;
+ Error_Msg_N ("\ found mode %", Item);
+ end Inconsistent_Mode_Error;
+
+ -- Start processing for Check_Matching_Modes
+
+ begin
+ if Contains (In_Items, Item_Id) then
+ if Global_Mode /= Name_Input then
+ Inconsistent_Mode_Error (Name_Input);
+ end if;
+
+ elsif Contains (In_Out_Items, Item_Id) then
+ if Global_Mode /= Name_In_Out then
+ Inconsistent_Mode_Error (Name_In_Out);
+ end if;
+
+ elsif Contains (Out_Items, Item_Id) then
+ if Global_Mode /= Name_Output then
+ Inconsistent_Mode_Error (Name_Output);
+ end if;
+
+ -- The item does not appear in the corresponding Global aspect,
+ -- it must be an extra.
+
+ else
+ Error_Msg_NE ("extra global item &", Item, Item_Id);
+ end if;
+ end Check_Matching_Modes;
+
+ ----------------
+ -- Is_Part_Of --
+ ----------------
+
+ function Is_Part_Of
+ (State : Entity_Id;
+ Ancestor : Entity_Id) return Boolean
+ is
+ Options : constant Node_Id := Parent (State);
+ Name : Node_Id;
+ Option : Node_Id;
+ Value : Node_Id;
+
+ begin
+ -- A state declaration with option Part_Of appears as an
+ -- extension aggregate with component associations.
+
+ if Nkind (Options) = N_Extension_Aggregate then
+ Option := First (Component_Associations (Options));
+ while Present (Option) loop
+ Name := First (Choices (Option));
+ Value := Expression (Option);
+
+ if Chars (Name) = Name_Part_Of then
+ return Entity (Value) = Ancestor;
+ end if;
+
+ Next (Option);
+ end loop;
+ end if;
+
+ return False;
+ end Is_Part_Of;
+
+ -- Local variables
+
+ Item_Id : constant Entity_Id := Entity_Of (Item);
+
+ -- Start of processing for Check_Refined_Global_Item
+
+ begin
+ -- State checks
+
+ if Ekind (Item_Id) = E_Abstract_State then
+
+ -- The state acts as a constituent of some other state. Ensure
+ -- that the other state is a proper ancestor of the item.
+
+ if Present (Refined_State (Item_Id)) then
+ if Is_Part_Of (Item_Id, Refined_State (Item_Id)) then
+ Add_Constituent (Item_Id);
+ else
+ Error_Msg_Name_1 := Chars (Refined_State (Item_Id));
+ Error_Msg_NE
+ ("state & is not a valid constituent of ancestor "
+ & "state %", Item, Item_Id);
+ end if;
+
+ -- An abstract state with visible refinement cannot appear in a
+ -- global refinement as its place must be taken by some of its
+ -- constituents.
+
+ elsif Present (Refinement_Constituents (Item_Id)) then
+ Error_Msg_NE
+ ("cannot mention state & in global refinement, use its "
+ & "constituents instead", Item, Item_Id);
+
+ -- The state is not refined nor is it a constituent. Ensure
+ -- that the modes of both its occurrences in Global and
+ -- Refined_Global match.
+
+ else
+ Check_Matching_Modes (Item_Id);
+ end if;
+
+ -- Variable checks
+
+ else pragma Assert (Ekind (Item_Id) = E_Variable);
+
+ -- The variable acts as a constituent of a state, collect it
+ -- for the state completeness checks performed later on.
+
+ if Present (Refined_State (Item_Id)) then
+ Add_Constituent (Item_Id);
+
+ -- The variable is not a constituent. Ensure that the modes of
+ -- both its occurrences in Global and Refined_Global match.
+
+ else
+ Check_Matching_Modes (Item_Id);
+ end if;
+ end if;
+ end Check_Refined_Global_Item;
+
+ -- Local variables
+
+ Item : Node_Id;
+
+ -- Start of processing for Check_Refined_Global_List
+
+ begin
+ -- Single global item declaration
+
+ if Nkind_In (List, N_Expanded_Name,
+ N_Identifier,
+ N_Selected_Component)
+ then
+ Check_Refined_Global_Item (List, Global_Mode);
+
+ -- Simple global list or moded global list declaration
+
+ elsif Nkind (List) = N_Aggregate then
+
+ -- The declaration of a simple global list appear as a collection
+ -- of expressions.
+
+ if Present (Expressions (List)) then
+ Item := First (Expressions (List));
+ while Present (Item) loop
+ Check_Refined_Global_Item (Item, Global_Mode);
+
+ Next (Item);
+ end loop;
+
+ -- The declaration of a moded global list appears as a collection
+ -- of component associations where individual choices denote
+ -- modes.
+
+ elsif Present (Component_Associations (List)) then
+ Item := First (Component_Associations (List));
+ while Present (Item) loop
+ Check_Refined_Global_List
+ (List => Expression (Item),
+ Global_Mode => Chars (First (Choices (Item))));
+
+ Next (Item);
+ end loop;
+
+ -- Invalid tree
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Invalid list
+
+ else
+ raise Program_Error;
+ end if;
+ end Check_Refined_Global_List;
+
+ --------------------------
+ -- Collect_Global_Items --
+ --------------------------
+
+ procedure Collect_Global_Items (Prag : Node_Id) is
+ procedure Process_Global_List
+ (List : Node_Id;
+ Mode : Name_Id := Name_Input);
+ -- Collect all items housed in a global list. Formal Mode denotes the
+ -- current mode in effect.
+
+ -------------------------
+ -- Process_Global_List --
+ -------------------------
+
+ procedure Process_Global_List
+ (List : Node_Id;
+ Mode : Name_Id := Name_Input)
+ is
+ procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id);
+ -- Add a single item to the appropriate list. Formal Mode denotes
+ -- the current mode in effect.
+
+ -------------------------
+ -- Process_Global_Item --
+ -------------------------
+
+ procedure Process_Global_Item (Item : Node_Id; Mode : Name_Id) is
+ Item_Id : constant Entity_Id := Entity_Of (Item);
+
+ begin
+ -- Signal that the global list contains at least one abstract
+ -- state with a visible refinement.
+
+ if Ekind (Item_Id) = E_Abstract_State
+ and then Present (Refinement_Constituents (Item_Id))
+ then
+ if Mode = Name_Input then
+ Has_In_State := True;
+ elsif Mode = Name_In_Out then
+ Has_In_Out_State := True;
+ elsif Mode = Name_Output then
+ Has_Out_State := True;
+ end if;
+ end if;
+
+ -- Add the item to the proper list
+
+ if Mode = Name_Input then
+ Add_Item (Item_Id, In_Items);
+ elsif Mode = Name_In_Out then
+ Add_Item (Item_Id, In_Out_Items);
+ elsif Mode = Name_Output then
+ Add_Item (Item_Id, Out_Items);
+ end if;
+ end Process_Global_Item;
+
+ -- Local variables
+
+ Item : Node_Id;
+
+ -- Start of processing for Process_Global_List
+
+ begin
+ -- Single global item declaration
+
+ if Nkind_In (List, N_Expanded_Name,
+ N_Identifier,
+ N_Selected_Component)
+ then
+ Process_Global_Item (List, Mode);
+
+ -- Single global list or moded global list declaration
+
+ elsif Nkind (List) = N_Aggregate then
+
+ -- The declaration of a simple global list appear as a
+ -- collection of expressions.
+
+ if Present (Expressions (List)) then
+ Item := First (Expressions (List));
+ while Present (Item) loop
+ Process_Global_Item (Item, Mode);
+
+ Next (Item);
+ end loop;
+
+ -- The declaration of a moded global list appears as a
+ -- collection of component associations where individual
+ -- choices denote modes.
+
+ elsif Present (Component_Associations (List)) then
+ Item := First (Component_Associations (List));
+ while Present (Item) loop
+ Process_Global_List
+ (List => Expression (Item),
+ Mode => Chars (First (Choices (Item))));
+
+ Next (Item);
+ end loop;
+
+ -- Invalid tree
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Invalid list
+
+ else
+ raise Program_Error;
+ end if;
+ end Process_Global_List;
+
+ -- Local variables
+
+ List : constant Node_Id :=
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
+
+ -- Start of processing for Collect_Global_Items
+
+ begin
+ -- Do not process a null global list as it contains nothing
+
+ if Nkind (List) /= N_Null then
+ Process_Global_List (List);
+ end if;
+ end Collect_Global_Items;
+
+ -------------------------
+ -- Present_Then_Remove --
+ -------------------------
+
+ function Present_Then_Remove
+ (List : Elist_Id;
+ Item : Entity_Id) return Boolean
+ is
+ Elmt : Elmt_Id;
+
+ begin
+ if Present (List) then
+ Elmt := First_Elmt (List);
+ while Present (Elmt) loop
+ if Node (Elmt) = Item then
+ Remove_Elmt (List, Elmt);
+ return True;
+ end if;
+
+ Next_Elmt (Elmt);
+ end loop;
+ end if;
+
+ return False;
+ end Present_Then_Remove;
+
+ -------------------------------
+ -- Report_Extra_Constituents --
+ -------------------------------
+
+ procedure Report_Extra_Constituents is
+ procedure Report_Extra_Constituents_In_List (List : Elist_Id);
+ -- Emit an error for every element of List
+
+ ---------------------------------------
+ -- Report_Extra_Constituents_In_List --
+ ---------------------------------------
+
+ procedure Report_Extra_Constituents_In_List (List : Elist_Id) is
+ Constit_Elmt : Elmt_Id;
+
+ begin
+ if Present (List) then
+ Constit_Elmt := First_Elmt (List);
+ while Present (Constit_Elmt) loop
+ Error_Msg_NE ("extra constituent &", N, Node (Constit_Elmt));
+ Next_Elmt (Constit_Elmt);
+ end loop;
+ end if;
+ end Report_Extra_Constituents_In_List;
+
+ -- Start of processing for Report_Extra_Constituents
+
+ begin
+ Report_Extra_Constituents_In_List (In_Constits);
+ Report_Extra_Constituents_In_List (In_Out_Constits);
+ Report_Extra_Constituents_In_List (Out_Constits);
+ end Report_Extra_Constituents;
+
+ -- Local variables
+
+ Body_Decl : constant Node_Id := Parent (N);
+ Errors : constant Nat := Serious_Errors_Detected;
+ List : constant Node_Id :=
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
+
+ -- Start of processing for Analyze_Refined_Global_In_Decl_Part
+
begin
- null;
+ Global := Get_Pragma (Spec_Id, Pragma_Global);
+
+ -- The subprogram declaration lacks aspect/pragma Global. This renders
+ -- Refined_Global useless as there is nothing to refine.
+
+ if No (Global) then
+ Error_Msg_NE
+ ("useless refinement, subprogram & lacks global items", N, Spec_Id);
+ return;
+ end if;
+
+ -- Extract all relevant items from the corresponding Global aspect or
+ -- pragma.
+
+ Collect_Global_Items (Global);
+
+ -- The corresponding Global aspect/pragma must mention at least one
+ -- state with a visible refinement at the point Refined_Global is
+ -- processed.
+
+ if not Has_In_State
+ and then not Has_In_Out_State
+ and then not Has_Out_State
+ then
+ Error_Msg_NE
+ ("useless refinement, subprogram & does not mention abstract state "
+ & "with visible refinement", N, Spec_Id);
+ return;
+ end if;
+
+ -- The global refinement of inputs and outputs cannot be null when the
+ -- corresponding Global aspect/pragma contains at least one item.
+
+ if Nkind (List) = N_Null
+ and then
+ (Present (In_Items)
+ or else Present (In_Out_Items)
+ or else Present (Out_Items))
+ then
+ Error_Msg_NE
+ ("refinement cannot be null, subprogram & has global items",
+ N, Spec_Id);
+ return;
+ end if;
+
+ -- Analyze Refined_Global as if it behaved as a regular aspect/pragma
+ -- Global. This ensures that the categorization of all refined global
+ -- items is consistent with their role.
+
+ Analyze_Global_In_Decl_Part (N);
+
+ -- Perform all refinement checks with respect to completeness and mode
+ -- matching.
+
+ if Serious_Errors_Detected = Errors then
+ Check_Refined_Global_List (List);
+ end if;
+
+ -- For Input states with visible refinement, at least one constituent
+ -- must be used as an Input in the global refinement.
+
+ if Serious_Errors_Detected = Errors then
+ Check_Input_States;
+ end if;
+
+ -- Verify all possible completion variants for In_Out states with
+ -- visible refinement.
+
+ if Serious_Errors_Detected = Errors then
+ Check_In_Out_States;
+ end if;
+
+ -- For Output states with visible refinement, all constituents must be
+ -- used as Outputs in the global refinement.
+
+ if Serious_Errors_Detected = Errors then
+ Check_Output_States;
+ end if;
+
+ -- Emit errors for all constituents that belong to other states with
+ -- visible refinement that do not appear in Global.
+
+ if Serious_Errors_Detected = Errors then
+ Report_Extra_Constituents;
+ end if;
end Analyze_Refined_Global_In_Decl_Part;
----------------------------------------
@@ -18587,6 +19493,9 @@
-------------------------------
procedure Analyze_Refinement_Clause (Clause : Node_Id) is
+ State_Id : Entity_Id := Empty;
+ -- The entity of the state being refined in the current clause
+
Non_Null_Seen : Boolean := False;
Null_Seen : Boolean := False;
-- Flags used to detect multiple uses of null in a single clause or a
@@ -18647,6 +19556,17 @@
Add_Item (Constit_Id, Constituents_Seen);
Remove_Elmt (Hidden_States, State_Elmt);
+ -- Establish a relation between the refined state and its
+ -- constituent.
+
+ if No (Refinement_Constituents (State_Id)) then
+ Set_Refinement_Constituents (State_Id, New_Elmt_List);
+ end if;
+
+ Append_Elmt
+ (Constit_Id, Refinement_Constituents (State_Id));
+ Set_Refined_State (Constit_Id, State_Id);
+
return;
end if;
@@ -18771,9 +19691,8 @@
-- Local declarations
- Constit : Node_Id;
- State : Node_Id;
- State_Id : Entity_Id := Empty;
+ Constit : Node_Id;
+ State : Node_Id;
-- Start of processing for Analyze_Refinement_Clause
@@ -18891,12 +19810,8 @@
-- Source objects (non-constants) are valid hidden states
- -- This is a very odd test, it misses many cases, e.g.
- -- renamings of objects, in-out parameters etc ???. Why
- -- not test the Ekind ???
-
if Nkind (Decl) = N_Object_Declaration
- and then not Constant_Present (Decl)
+ and then Ekind (Defining_Entity (Decl)) = E_Variable
and then Comes_From_Source (Decl)
then
Add_Item (Defining_Entity (Decl), Result);
@@ -19004,7 +19919,7 @@
-- Initialize the various lists used during analysis
- Abstr_States := Clone (Abstract_States (Spec_Id));
+ Abstr_States := New_Copy_Elist (Abstract_States (Spec_Id));
Hidden_States := Collect_Hidden_States;
-- Multiple state refinements appear as an aggregate
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 203503)
+++ sem_util.adb (revision 203504)
@@ -27,8 +27,8 @@
with Casing; use Casing;
with Checks; use Checks;
with Debug; use Debug;
+with Elists; use Elists;
with Errout; use Errout;
-with Elists; use Elists;
with Exp_Ch11; use Exp_Ch11;
with Exp_Disp; use Exp_Disp;
with Exp_Util; use Exp_Util;
@@ -3157,6 +3157,127 @@
end if;
end Conditional_Delay;
+ ----------------------------
+ -- Contains_Refined_State --
+ ----------------------------
+
+ function Contains_Refined_State (Prag : Node_Id) return Boolean is
+ function Has_Refined_State (List : Node_Id) return Boolean;
+ -- Determine whether a global list mentions a state with a visible
+ -- refinement.
+
+ -----------------------
+ -- Has_Refined_State --
+ -----------------------
+
+ function Has_Refined_State (List : Node_Id) return Boolean is
+ function Is_Refined_State (Item : Node_Id) return Boolean;
+ -- Determine whether Item is a reference to an abstract state with a
+ -- visible refinement.
+
+ ----------------------
+ -- Is_Refined_State --
+ ----------------------
+
+ function Is_Refined_State (Item : Node_Id) return Boolean is
+ Item_Id : Entity_Id;
+
+ begin
+ if Nkind (Item) = N_Null then
+ return False;
+
+ else
+ Item_Id := Entity_Of (Item);
+
+ return
+ Ekind (Item_Id) = E_Abstract_State
+ and then Present (Refinement_Constituents (Item_Id));
+ end if;
+ end Is_Refined_State;
+
+ -- Local variables
+
+ Item : Node_Id;
+
+ -- Start of processing for Has_Refined_State
+
+ begin
+ -- A null global list does not mention any states
+
+ if Nkind (List) = N_Null then
+ return False;
+
+ -- Single global item declaration
+
+ elsif Nkind_In (List, N_Expanded_Name,
+ N_Identifier,
+ N_Selected_Component)
+ then
+ return Is_Refined_State (List);
+
+ -- Simple global list or moded global list declaration
+
+ elsif Nkind (List) = N_Aggregate then
+
+ -- The declaration of a simple global list appear as a collection
+ -- of expressions.
+
+ if Present (Expressions (List)) then
+ Item := First (Expressions (List));
+ while Present (Item) loop
+ if Is_Refined_State (Item) then
+ return True;
+ end if;
+
+ Next (Item);
+ end loop;
+
+ -- The declaration of a moded global list appears as a collection
+ -- of component associations where individual choices denote
+ -- modes.
+
+ else
+ Item := First (Component_Associations (List));
+ while Present (Item) loop
+ if Has_Refined_State (Expression (Item)) then
+ return True;
+ end if;
+
+ Next (Item);
+ end loop;
+ end if;
+
+ -- If we get here, then the simple/moded global list did not
+ -- mention any states with a visible refinement.
+
+ return False;
+
+ -- Something went horribly wrong, we have a malformed tree
+
+ else
+ raise Program_Error;
+ end if;
+ end Has_Refined_State;
+
+ -- Local variables
+
+ Arg : constant Node_Id :=
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
+ Nam : constant Name_Id := Pragma_Name (Prag);
+
+ -- Start of processing for Contains_Refined_State
+
+ begin
+ -- ??? To be implemented
+
+ if Nam = Name_Depends then
+ return False;
+
+ else pragma Assert (Nam = Name_Global);
+ return Has_Refined_State (Arg);
+ end if;
+ end Contains_Refined_State;
+
-------------------------
-- Copy_Component_List --
-------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 203503)
+++ sem_util.ads (revision 203504)
@@ -326,6 +326,13 @@
-- Sets the Has_Delayed_Freeze flag of New if the Delayed_Freeze flag of
-- Old is set and Old has no yet been Frozen (i.e. Is_Frozen is false).
+ function Contains_Refined_State (Prag : Node_Id) return Boolean;
+ -- Determine whether pragma Prag contains a reference to the entity of an
+ -- abstract state with a visible refinement. Prag must denote one of the
+ -- following pragmas:
+ -- Depends
+ -- Global
+
function Copy_Parameter_List (Subp_Id : Entity_Id) return List_Id;
-- Utility to create a parameter profile for a new subprogram spec, when
-- the subprogram has a body that acts as spec. This is done for some cases
Index: elists.adb
===================================================================
--- elists.adb (revision 203503)
+++ elists.adb (revision 203504)
@@ -158,34 +158,6 @@
end loop;
end Append_Unique_Elmt;
- -----------
- -- Clone --
- ------------
-
- function Clone (List : Elist_Id) return Elist_Id is
- Result : Elist_Id;
- Elmt : Elmt_Id;
-
- begin
- if List = No_Elist then
- return No_Elist;
-
- -- Replicate the contents of the input list while preserving the
- -- original order.
-
- else
- Result := New_Elmt_List;
-
- Elmt := First_Elmt (List);
- while Present (Elmt) loop
- Append_Elmt (Node (Elmt), Result);
- Next_Elmt (Elmt);
- end loop;
-
- return Result;
- end if;
- end Clone;
-
--------------
-- Contains --
--------------
@@ -315,6 +287,34 @@
Elmts.Release;
end Lock;
+ --------------------
+ -- New_Copy_Elist --
+ --------------------
+
+ function New_Copy_Elist (List : Elist_Id) return Elist_Id is
+ Result : Elist_Id;
+ Elmt : Elmt_Id;
+
+ begin
+ if List = No_Elist then
+ return No_Elist;
+
+ -- Replicate the contents of the input list while preserving the
+ -- original order.
+
+ else
+ Result := New_Elmt_List;
+
+ Elmt := First_Elmt (List);
+ while Present (Elmt) loop
+ Append_Elmt (Node (Elmt), Result);
+ Next_Elmt (Elmt);
+ end loop;
+
+ return Result;
+ end if;
+ end New_Copy_Elist;
+
-------------------
-- New_Elmt_List --
-------------------
@@ -425,6 +425,27 @@
return Elmt /= No_Elmt;
end Present;
+ ------------
+ -- Remove --
+ ------------
+
+ procedure Remove (List : Elist_Id; N : Node_Or_Entity_Id) is
+ Elmt : Elmt_Id;
+
+ begin
+ if Present (List) then
+ Elmt := First_Elmt (List);
+ while Present (Elmt) loop
+ if Node (Elmt) = N then
+ Remove_Elmt (List, Elmt);
+ exit;
+ end if;
+
+ Next_Elmt (Elmt);
+ end loop;
+ end if;
+ end Remove;
+
-----------------
-- Remove_Elmt --
-----------------
Index: elists.ads
===================================================================
--- elists.ads (revision 203503)
+++ elists.ads (revision 203504)
@@ -137,12 +137,20 @@
-- Add a new element (N) right after the pre-existing element Elmt
-- It is invalid to call this subprogram with Elmt = No_Elmt.
+ function New_Copy_Elist (List : Elist_Id) return Elist_Id;
+ -- Replicate the contents of a list. Internal list nodes are not shared and
+ -- order of elements is preserved.
+
procedure Replace_Elmt (Elmt : Elmt_Id; New_Node : Node_Or_Entity_Id);
pragma Inline (Replace_Elmt);
-- Causes the given element of the list to refer to New_Node, the node
-- which was previously referred to by Elmt is effectively removed from
-- the list and replaced by New_Node.
+ procedure Remove (List : Elist_Id; N : Node_Or_Entity_Id);
+ -- Remove a node or an entity from a list. If the list does not contain the
+ -- item in question, the routine has no effect.
+
procedure Remove_Elmt (List : Elist_Id; Elmt : Elmt_Id);
-- Removes Elmt from the given list. The node itself is not affected,
-- but the space used by the list element may be (but is not required
@@ -153,10 +161,6 @@
-- affected, but the space used by the list element may be (but is not
-- required to be) freed for reuse in a subsequent Append_Elmt call.
- function Clone (List : Elist_Id) return Elist_Id;
- -- Create a copy of the input list. Internal list nodes are not shared and
- -- order of elements is preserved.
-
function Contains (List : Elist_Id; N : Node_Or_Entity_Id) return Boolean;
-- Perform a sequential search to determine whether the given list contains
-- a node or an entity.
Index: ChangeLog
===================================================================
--- ChangeLog (revision 203503)
+++ ChangeLog (revision 203504)
@@ -1,3 +1,68 @@
+2013-10-13 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * einfo.adb: Add node/list usage for Refined_State
+ and Refinement_Constituents.
+ (Get_Pragma): Update the
+ initialization of Is_CDG to include Refined_Global and
+ Refined_Depends. Rename constant Delayed to In_Contract and update
+ all of its occurrences.
+ (Is_Non_Volatile_State): New routine.
+ (Is_Volatile_State): Removed.
+ (Refined_State): New routine.
+ (Refinement_Constituents): New routine.
+ (Set_Refined_State): New routine.
+ (Set_Refinement_Constituents): New routine.
+ (Write_Field8_Name): Add output for Refinement_Constituents.
+ (Write_Field10_Name): Add output for Refined_State.
+ * einfo.ads: Add new synthesized attribute Is_Non_Volatile_State.
+ Remove synthesized attribute Is_Volatile_State. Add new
+ attributes Refined_State and Refinement_Constituents along with
+ usage in nodes.
+ (Get_Pragma): Update the comment on usage.
+ (Is_Non_Volatile_State): New routine.
+ (Is_Volatile_State): Removed.
+ (Refined_State): New routine and pragma Inline.
+ (Refinement_Constituents): New routine and pragma Inline.
+ (Set_Refined_State): New routine and pragma Inline.
+ (Set_Refinement_Constituents): New routine and pragma Inline.
+ * elists.ads, elists.adb (Clone): Removed.
+ (New_Copy_Elist): New routine.
+ (Remove): New routine.
+ * sem_ch3.adb (Analyze_Declarations): Use Defining_Entity
+ to get the entity of the subprogram [body].
+ (Analyze_Object_Declaration): Add initialization for
+ Refined_State.
+ * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add processing
+ for Refined_Global and Refined_Depends. Emit an error when
+ the body requires Refined_Global, but the aspect/pragma is
+ not present.
+ * sem_ch6.ads (Analyze_Subprogram_Body_Contract): Change
+ procedure signature and add comment on usage.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
+ for aspect Refined_Global.
+ * sem_prag.adb (Analyze_Abstract_State): Add initialization
+ of attributes Refined_State and Refinement_Constituents.
+ (Analyze_Depends_In_Decl_Part, Analyze_Global_In_Decl_Part,
+ Analyze_Contract_Cases_In_Decl_Part): Remove local
+ constant Arg1.
+ (Analyze_Pragma): Add processing for pragma
+ Refined_Global. The analysis of Refined_Post and Refined_Pre
+ has been merged. Update an error message in the processing of
+ pragma Refined_State.
+ (Analyze_Refined_Global_In_Decl_Part): Provide implementation.
+ (Analyze_Refined_Pragma): New routine.
+ (Analyze_Refined_Pre_Post_Condition): Removed.
+ (Analyze_Refined_State_In_Decl_Part): Update the call to Clone.
+ (Analyze_Refinement_Clause): Make State_Id visible to all
+ nested subprogram.
+ (Check_Matching_Constituent): Establish
+ a relation between a refined state and its constituent.
+ (Collect_Hidden_States_In_Decls): Remove ??? comment. Look at
+ the entity of the object declaration to establish its kind.
+ * sem_util.adb: Alphabetize with and use clauses.
+ (Contains_Refined_State): New routine.
+ * sem_util.ads (Contains_Refined_State): New routine.
+
2013-10-13 Thomas Quinot <quinot@adacore.com>
* scos.ads: Minor documentation clarification.
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 203503)
+++ sem_ch6.adb (revision 203504)
@@ -1975,12 +1975,47 @@
-- Analyze_Subprogram_Body_Contract --
--------------------------------------
- -- ??? To be implemented
+ procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
+ Body_Decl : constant Node_Id := Parent (Parent (Body_Id));
+ Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
+ Prag : Node_Id;
- procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id) is
- pragma Unreferenced (Subp);
+ Has_Refined_Global : Boolean := False;
+
begin
- null;
+ -- When a subprogram body declaration is erroneous, its defining entity
+ -- is left unanalyzed. There is nothing left to do in this case because
+ -- the body lacks a contract.
+
+ if not Analyzed (Body_Id) then
+ return;
+ end if;
+
+ Prag := Classifications (Contract (Body_Id));
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Refined_Depends then
+ Analyze_Refined_Depends_In_Decl_Part (Prag);
+
+ elsif Pragma_Name (Prag) = Name_Refined_Global then
+ Has_Refined_Global := True;
+ Analyze_Refined_Global_In_Decl_Part (Prag);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- When the corresponding Global aspect/pragma references a state with
+ -- visible refinement, the body requires Refined_Global.
+
+ if not Has_Refined_Global and then Present (Spec_Id) then
+ Prag := Get_Pragma (Spec_Id, Pragma_Global);
+
+ if Present (Prag) and then Contains_Refined_State (Prag) then
+ Error_Msg_NE
+ ("body of subprogram & requires global refinement",
+ Body_Decl, Spec_Id);
+ end if;
+ end if;
end Analyze_Subprogram_Body_Contract;
------------------------------------
Index: sem_ch6.ads
===================================================================
--- sem_ch6.ads (revision 203503)
+++ sem_ch6.ads (revision 203504)
@@ -46,10 +46,10 @@
procedure Analyze_Subprogram_Declaration (N : Node_Id);
procedure Analyze_Subprogram_Body (N : Node_Id);
- procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id);
+ procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id);
-- Analyze all delayed aspects chained on the contract of subprogram body
- -- Subp as if they appeared at the end of a declarative region. The aspects
- -- in question are:
+ -- Body_Id as if they appeared at the end of a declarative region. The
+ -- aspects in question are:
-- Refined_Depends
-- Refined_Global
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 203503)
+++ sem_ch13.adb (revision 203504)
@@ -1977,11 +1977,22 @@
-- Refined_Global
- -- ??? To be implemented
+ -- Aspect Refined_Global must be delayed because it can mention
+ -- state refinements introduced by aspect Refined_State. Since
+ -- Refined_State is already delayed due to forward references,
+ -- so is Refined_Global.
when Aspect_Refined_Global =>
- null;
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Refined_Global);
+ Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
+ Insert_Delayed_Pragma (Aitem);
+ goto Continue;
+
-- Refined_Post
when Aspect_Refined_Post =>
More information about the Gcc-patches
mailing list