This patch provides the initial implementation of aspect/pragma Refined_State.
The construct is intended for formal verification proofs.
The syntax of the aspect/pragma is as follows:
pragma Refined_State (REFINEMENT_LIST);
REFINEMENT_LIST ::=
REFINEMENT_CLAUSE
| (REFINEMENT_CLAUSE {, REFINEMENT_CLAUSE})
REFINEMENT_CLAUSE ::= state_NAME => CONSTITUENT_LIST
CONSTITUENT_LIST ::=
null
| CONSTITUENT
| (CONSTITUENT {, CONSTITUENT})
CONSTITUENT ::= object_NAME | state_NAME
The semantics of the aspect/pragma are as follows:
A Refined_State aspect may only appear in the aspect_specification of a
package_body. [The use of package_body rather than package body allows this
aspect to be specified for generic package bodies.]
If a package_specification has a non-null Abstract_State aspect its body shall
have a Refined_State aspect.
If a package_specification does not have an Abstract_State aspect, then the
corresponding package_body shall not have a Refined_State aspect.
A Refined_State Aspect of a package_body has visibility extended to the
declarative_part of the body.
Each constituent is either a variable or a state abstraction.
An object which is a constituent shall be an entire object.
Each abstract_state_name declared in the package specification shall be denoted
as the state_name of a refinement_clause in the Refined_State aspect of the
body of the package.
Every entity of the hidden state of a package shall be denoted as a constituent
of exactly one abstract_state_name in the Refined_State aspect of the package
and shall not be denoted more than once. [These constituents are either
variables declared in the private part or body of the package, or the
declarations from the visible part of nested packages declared immediately
therein.]
------------
-- Source --
------------
-- semantics.ads
package Semantics
with Abstract_State =>
((Refinement_State_1 with External, Input_Only),
(Refinement_State_2 with External, Output_Only),
(Refinement_State_3 with Non_Volatile),
(Refinement_State_4 with Non_Volatile)) -- not refined
is
procedure Enforce_Body;
Var_1 : Integer;
package In_Visible_Part
with Abstract_State =>
(State_1 with External, Input_Only)
is
Var_2 : Integer;
private
Var_3 : Integer;
end In_Visible_Part;
package Has_AS_No_RS
with Abstract_State =>
(Has_AS_No_RS_State with Non_Volatile)
is end Has_AS_No_RS;
package Null_AS_No_RS
with Abstract_State => null
is end Null_AS_No_RS;
package No_AS_Has_RS
with Abstract_State =>
(No_AS_Has_RS_State with Non_Volatile)
is end No_AS_Has_RS;
private
Var_4 : Integer;
Extra_1 : Integer; -- hidden state not used
package In_Private_Part
with Abstract_State =>
(State_2 with External, Output_Only)
is
Var_5 : Integer;
private
Var_6 : Integer;
end In_Private_Part;
end Semantics;
-- semantics.adb
package body Semantics
with Refined_State =>
(Refinement_State_1 =>
(Var_1, -- not a hidden state
In_Visible_Part.State_1, -- not a hidden state
In_Visible_Part.Var_2, -- not a hidden state
In_Visible_Part.Var_3), -- not a hidden state
Refinement_State_2 =>
(Var_4,
In_Private_Part.State_2,
In_Private_Part.Var_5,
In_Private_Part.Var_6, -- not a hidden state
In_Private_Part.State_2), -- duplicate use of hidden state
Refinement_State_3 =>
(Var_7,
In_Body.State_3,
In_Body.Var_8,
In_Body.Var_9, -- not a hidden state
Var_7), -- duplicate use of hidden state
Refinement_State_2 => null, -- duplicate refinement
In_Visible_Part.State_1 => null) -- not a valid abstract state of
-- package Semantics
is
procedure Enforce_Body is begin null; end Enforce_Body;
package body In_Visible_Part
with Refined_State => (State_1 => Var_3)
is end In_Visible_Part;
package body Has_AS_No_RS is end Has_AS_No_RS; -- requires refinement
package body Null_AS_No_RS is end Null_AS_No_RS;
package body No_AS_Has_RS
with Refined_State => (No_AS_Has_RS_State => null) -- useless
is end No_AS_Has_RS; -- refinement
package body In_Private_Part
with Refined_State => (State_2 => Var_6)
is end In_Private_Part;
Var_7 : Integer;
package In_Body
with Abstract_State =>
(State_3 with Non_Volatile)
is
Var_8 : Integer;
Extra_2 : Integer; -- hidden state not used
private
Var_9 : Integer;
end In_Body;
package body In_Body
with Refined_State => (State_3 => Var_9)
is end In_Body;
end Semantics;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnat12 -gnatd.V semantics.adb
semantics.adb:2:08: package "Semantics" has unused hidden states
semantics.adb:2:08: variable "Extra_1" defined at semantics.ads:37
semantics.adb:2:08: variable "Extra_2" defined at line 53
semantics.adb:4:14: cannot use "Var_1" in refinement, constituent is not a
hidden state of package "Semantics"
semantics.adb:5:29: cannot use "State_1" in refinement, constituent is not a
hidden state of package "Semantics"
semantics.adb:6:29: cannot use "Var_2" in refinement, constituent is not a
hidden state of package "Semantics"
semantics.adb:7:29: "Var_3" is not a visible entity of "In_Visible_Part"
semantics.adb:13:29: "Var_6" is not a visible entity of "In_Private_Part"
semantics.adb:14:29: duplicate use of constituent "State_2"
semantics.adb:20:21: "Var_9" is not a visible entity of "In_Body"
semantics.adb:21:14: duplicate use of constituent "Var_7"
semantics.adb:23:11: duplicate refinement of state "Refinement_State_2"
semantics.adb:25:26: cannot refine state, "State_1" is not defined in package
"Semantics"
semantics.adb:34:04: package "Has_AS_No_RS" requires state refinement
semantics.ads:6:11: abstract state "Refinement_State_4" must be refined
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-10-10 Hristian Kirtchev <kirtc...@adacore.com>
* aspects.adb: Add an entry in table Canonical_Aspect for
Refined_State.
* aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
Aspect_Names and Aspect_Delay for Refined_State.
* einfo.adb: Add with and use clauses for Elists.
Remove Refined_State from the list of node usage.
Add Refined_State_Pragma to the list of node usage.
(Has_Null_Abstract_State): New routine.
(Refined_State): Removed.
(Refined_State_Pragma): New routine.
(Set_Refined_State): Removed.
(Set_Refined_State_Pragma): New routine.
(Write_Field8_Name): Add output for Refined_State_Pragma.
(Write_Field9_Name): Remove the output for Refined_State.
* einfo.ads: Add new synthesized attribute Has_Null_Abstract_State
along with usage in nodes. Remove attribute Refined_State along
with usage in nodes. Add new attribute Refined_State_Pragma along
with usage in nodes.
(Has_Null_Abstract_State): New routine.
(Refined_State): Removed.
(Refined_State_Pragma): New routine.
(Set_Refined_State): Removed.
(Set_Refined_State_Pragma): New routine.
* elists.adb (Clone): New routine.
* elists.ads (Clone): New routine.
* par-prag.adb: Add Refined_State to the pragmas that do not
require special processing by the parser.
* sem_ch3.adb: Add with and use clause for Sem_Prag.
(Analyze_Declarations): Add local variables Body_Id, Context and
Spec_Id. Add processing for delayed aspect/pragma Refined_State.
* sem_ch13.adb (Analyze_Aspect_Specifications): Update the
handling of aspect Abstract_State. Add processing for aspect
Refined_State. Remove the bizzare insertion policy for aspect
Abstract_State.
(Check_Aspect_At_Freeze_Point): Add an entry for Refined_State.
* sem_prag.adb: Add an entry to table Sig_Flags
for pragma Refined_State.
(Add_Item): Update the
comment on usage. The inserted items need not be unique.
(Analyze_Contract_Cases_In_Decl_Part): Rename variable Restore to
Restore_Scope and update all its occurrences.
(Analyze_Pragma):
Update the handling of pragma Abstract_State. Add processing for
pragma Refined_State.
(Analyze_Pre_Post_Condition_In_Decl_Part):
Rename variable Restore to Restore_Scope and update all its
occurrences.
(Analyze_Refined_State_In_Decl_Part): New routine.
* sem_prag.ads (Analyze_Refined_State_In_Decl_Part): New routine.
* snames.ads-tmpl: Add new predefined name for Refined_State. Add
new Pragma_Id for Refined_State.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 203365)
+++ sem_ch3.adb (working copy)
@@ -64,6 +64,7 @@
with Sem_Elim; use Sem_Elim;
with Sem_Eval; use Sem_Eval;
with Sem_Mech; use Sem_Mech;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Smem; use Sem_Smem;
with Sem_Type; use Sem_Type;
@@ -2079,8 +2080,11 @@
-- Local variables
+ Body_Id : Entity_Id;
+ Context : Node_Id;
Freeze_From : Entity_Id := Empty;
Next_Decl : Node_Id;
+ Spec_Id : Entity_Id;
-- Start of processing for Analyze_Declarations
@@ -2190,6 +2194,37 @@
Decl := Next_Decl;
end loop;
+ -- Analyze the state refinements within a package body now, after all
+ -- hidden states have been encountered and freely visible. Refinements
+ -- must be processed before pragmas Refined_Depends and Refined_Global
+ -- because the last two may mention constituents.
+
+ if Present (L) then
+ Context := Parent (L);
+
+ if Nkind (Context) = N_Package_Body then
+ Body_Id := Defining_Entity (Context);
+ Spec_Id := Corresponding_Spec (Context);
+
+ -- The analysis of pragma Refined_State detects whether the spec
+ -- has abstract states available for refinement.
+
+ if Present (Refined_State_Pragma (Body_Id)) then
+ Analyze_Refined_State_In_Decl_Part
+ (Refined_State_Pragma (Body_Id));
+
+ -- State refinement is required when the package declaration has
+ -- abstract states. Null states are not considered.
+
+ elsif Present (Abstract_States (Spec_Id))
+ and then not Has_Null_Abstract_State (Spec_Id)
+ then
+ Error_Msg_NE
+ ("package & requires state refinement", Context, Spec_Id);
+ end if;
+ end if;
+ end if;
+
-- Analyze the contracts of a subprogram declaration or a body now due
-- to delayed visibility requirements of aspects.
Index: einfo.adb
===================================================================
--- einfo.adb (revision 203370)
+++ einfo.adb (working copy)
@@ -33,6 +33,7 @@
-- Turn off subprogram ordering, not used for this unit
with Atree; use Atree;
+with Elists; use Elists;
with Namet; use Namet;
with Nlists; use Nlists;
with Output; use Output;
@@ -79,12 +80,12 @@
-- Mechanism Uint8 (but returns Mechanism_Type)
-- Normalized_First_Bit Uint8
-- Postcondition_Proc Node8
+ -- Refined_State_Pragma Node8
-- Return_Applies_To Node8
-- First_Exit_Statement Node8
-- Class_Wide_Type Node9
-- Current_Value Node9
- -- Refined_State Node9
-- Renaming_Map Uint9
-- Direct_Primitive_Operations Elist10
@@ -2647,11 +2648,11 @@
return Flag227 (Id);
end Referenced_As_Out_Parameter;
- function Refined_State (Id : E) return E is
+ function Refined_State_Pragma (Id : E) return N is
begin
- pragma Assert (Ekind (Id) = E_Abstract_State);
- return Node9 (Id);
- end Refined_State;
+ pragma Assert (Ekind (Id) = E_Package_Body);
+ return Node8 (Id);
+ end Refined_State_Pragma;
function Register_Exception_Call (Id : E) return N is
begin
@@ -5307,11 +5308,11 @@
Set_Flag227 (Id, V);
end Set_Referenced_As_Out_Parameter;
- procedure Set_Refined_State (Id : E; V : E) is
+ procedure Set_Refined_State_Pragma (Id : E; V : N) is
begin
- pragma Assert (Ekind (Id) = E_Abstract_State);
- Set_Node9 (Id, V);
- end Set_Refined_State;
+ pragma Assert (Ekind (Id) = E_Package_Body);
+ Set_Node8 (Id, V);
+ end Set_Refined_State_Pragma;
procedure Set_Register_Exception_Call (Id : E; V : N) is
begin
@@ -6427,6 +6428,19 @@
return False;
end Has_Interrupt_Handler;
+ -----------------------------
+ -- Has_Null_Abstract_State --
+ -----------------------------
+
+ function Has_Null_Abstract_State (Id : E) return B is
+ begin
+ pragma Assert (Ekind_In (Id, E_Generic_Package, E_Package));
+
+ return
+ Present (Abstract_States (Id))
+ and then Is_Null_State (Node (First_Elmt (Abstract_States (Id))));
+ end Has_Null_Abstract_State;
+
--------------------
-- Has_Unmodified --
--------------------
@@ -8292,6 +8306,9 @@
when E_Procedure =>
Write_Str ("Postcondition_Proc");
+ when E_Package_Body =>
+ Write_Str ("Refined_State_Pragma");
+
when E_Return_Statement =>
Write_Str ("Return_Applies_To");
@@ -8313,9 +8330,6 @@
when Object_Kind =>
Write_Str ("Current_Value");
- when E_Abstract_State =>
- Write_Str ("Refined_State");
-
when E_Function |
E_Generic_Function |
E_Generic_Package |
Index: einfo.ads
===================================================================
--- einfo.ads (revision 203368)
+++ einfo.ads (working copy)
@@ -1645,6 +1645,10 @@
-- are not considered to be significant since they do not affect
-- stored bit patterns.
+-- Has_Null_Abstract_State (synth)
+-- Defined in package entities. True if the package is subject to a null
+-- Abstract_State aspect/pragma.
+
-- Has_Object_Size_Clause (Flag172)
-- Defined in entities for types and subtypes. Set if an Object_Size
-- clause has been processed for the type Used to prevent multiple
@@ -3533,9 +3537,9 @@
-- we have a separate warning for variables that are only assigned and
-- never read, and out parameters are a special case.
--- Refined_State (Node9)
--- Defined in E_Abstract_State entities. Contains the entity of the
--- abstract state completion which is usually foung in package bodies.
+-- Refined_State_Pragma (Node8)
+-- Defined in [generic] package bodies. Contains the pragma that refines
+-- all abstract states defined in the corresponding package declaration.
-- Register_Exception_Call (Node20)
-- Defined in exception entities. When an exception is declared,
@@ -5092,7 +5096,6 @@
------------------------------------------
-- E_Abstract_State
- -- Refined_State (Node9)
-- Is_External_State (synth)
-- Is_Input_Only_State (synth)
-- Is_Null_State (synth)
@@ -5636,10 +5639,12 @@
-- Is_Visible_Lib_Unit (Flag116)
-- Renamed_In_Spec (Flag231) (non-generic case only)
-- Static_Elaboration_Desired (Flag77) (non-generic case only)
+ -- Has_Null_Abstract_State (synth)
-- Is_Wrapper_Package (synth) (non-generic case only)
-- Scope_Depth (synth)
-- E_Package_Body
+ -- Refined_State_Pragma (Node8)
-- Handler_Records (List10) (non-generic case only)
-- Related_Instance (Node15) (non-generic case only)
-- First_Entity (Node17)
@@ -6535,7 +6540,7 @@
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 Register_Exception_Call (Id : E) return N;
function Related_Array_Object (Id : E) return E;
function Related_Expression (Id : E) return N;
@@ -6674,6 +6679,7 @@
function Has_Attach_Handler (Id : E) return B;
function Has_Entries (Id : E) return B;
function Has_Foreign_Convention (Id : E) return B;
+ function Has_Null_Abstract_State (Id : E) return B;
function Implementation_Base_Type (Id : E) return E;
function Is_Base_Type (Id : E) return B;
function Is_Boolean_Type (Id : E) return B;
@@ -7152,7 +7158,7 @@
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_Register_Exception_Call (Id : E; V : N);
procedure Set_Related_Array_Object (Id : E; V : E);
procedure Set_Related_Expression (Id : E; V : N);
@@ -7902,7 +7908,7 @@
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 (Register_Exception_Call);
pragma Inline (Related_Array_Object);
pragma Inline (Related_Expression);
@@ -8318,7 +8324,7 @@
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_Register_Exception_Call);
pragma Inline (Set_Related_Array_Object);
pragma Inline (Set_Related_Expression);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 203365)
+++ sem_prag.adb (working copy)
@@ -168,9 +168,9 @@
-------------------------------------
procedure Add_Item (Item : Entity_Id; To_List : in out Elist_Id);
- -- Subsidiary routine to the analysis of pragmas Depends and Global. Append
- -- an input or output item to a list. If the list is empty, a new one is
- -- created.
+ -- Subsidiary routine to the analysis of pragmas Depends, Global and
+ -- Refined_State. Append an entity to a list. If the list is empty, create
+ -- a new list.
function Adjust_External_Name_Case (N : Node_Id) return Node_Id;
-- This routine is used for possible casing adjustment of an explicit
@@ -285,7 +285,7 @@
To_List := New_Elmt_List;
end if;
- Append_Unique_Elmt (Item, To_List);
+ Append_Elmt (Item, To_List);
end Add_Item;
-------------------------------
@@ -404,10 +404,12 @@
Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
All_Cases : Node_Id;
CCase : Node_Id;
- Restore : Boolean := False;
Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
+ Restore_Scope : Boolean := False;
+ -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
+
-- Start of processing for Analyze_Contract_Cases_In_Decl_Part
begin
@@ -432,7 +434,7 @@
-- for subprogram bodies because the formals are already visible.
if Requires_Profile_Installation (N, Subp_Decl) then
- Restore := True;
+ Restore_Scope := True;
Push_Scope (Subp_Id);
Install_Formals (Subp_Id);
end if;
@@ -443,7 +445,7 @@
Next (CCase);
end loop;
- if Restore then
+ if Restore_Scope then
End_Scope;
end if;
end if;
@@ -8494,7 +8496,6 @@
Set_Parent (Id, State);
Set_Ekind (Id, E_Abstract_State);
Set_Etype (Id, Standard_Void_Type);
- Set_Refined_State (Id, Empty);
-- Every non-null state must be nameable and resolvable the
-- same way a constant is.
@@ -8523,8 +8524,8 @@
-- Local variables
- Par : Node_Id;
- State : Node_Id;
+ Context : constant Node_Id := Parent (Parent (N));
+ State : Node_Id;
-- Start of processing for Abstract_State
@@ -8536,24 +8537,14 @@
-- Ensure the proper placement of the pragma. Abstract states must
-- be associated with a package declaration.
- if From_Aspect_Specification (N) then
- Par := Parent (Corresponding_Aspect (N));
- else
- Par := Parent (Parent (N));
- end if;
-
- if Nkind (Par) = N_Compilation_Unit then
- Par := Unit (Par);
- end if;
-
- if not Nkind_In (Par, N_Generic_Package_Declaration,
- N_Package_Declaration)
+ if not Nkind_In (Context, N_Generic_Package_Declaration,
+ N_Package_Declaration)
then
Pragma_Misplaced;
return;
end if;
- Pack_Id := Defining_Entity (Par);
+ Pack_Id := Defining_Entity (Context);
State := Expression (Arg1);
-- Multiple abstract states appear as an aggregate
@@ -15974,6 +15965,62 @@
when Pragma_Refined_Pre =>
Analyze_Refined_Pre_Post_Condition;
+ -------------------
+ -- Refined_State --
+ -------------------
+
+ -- pragma Refined_State (REFINEMENT_LIST);
+
+ -- REFINEMENT_LIST ::=
+ -- REFINEMENT_CLAUSE
+ -- | (REFINEMENT_CLAUSE {, REFINEMENT_CLAUSE})
+
+ -- REFINEMENT_CLAUSE ::= state_NAME => CONSTITUENT_LIST
+
+ -- CONSTITUENT_LIST ::=
+ -- null
+ -- | CONSTITUENT
+ -- | (CONSTITUENT {, CONSTITUENT})
+
+ -- CONSTITUENT ::= object_NAME | state_NAME
+
+ when Pragma_Refined_State => Refined_State : declare
+ Context : constant Node_Id := Parent (N);
+ Spec_Id : Entity_Id;
+
+ begin
+ GNAT_Pragma;
+ S14_Pragma;
+ Check_Arg_Count (1);
+
+ -- Ensure the proper placement of the pragma. Refined states must
+ -- be associated with a package body.
+
+ if Nkind (Context) /= N_Package_Body then
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ -- State refinement is allowed only when the corresponding package
+ -- declaration has a non-null aspect/pragma Abstract_State.
+
+ Spec_Id := Corresponding_Spec (Context);
+
+ 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");
+ return;
+ end if;
+
+ -- The pragma must be analyzed at the end of the declarations as
+ -- it has visibility over the whole declarative region. Save the
+ -- pragma for later (see Analyze_Refined_Depends_In_Decl_Part).
+
+ Set_Refined_State_Pragma (Defining_Entity (Context), N);
+ end Refined_State;
+
-----------------------
-- Relative_Deadline --
-----------------------
@@ -18313,17 +18360,18 @@
(Prag : Node_Id;
Subp_Id : Entity_Id)
is
- Arg1 : constant Node_Id :=
- First (Pragma_Argument_Associations (Prag));
- Expr : Node_Id;
- Restore : Boolean := False;
+ Arg1 : constant Node_Id := First (Pragma_Argument_Associations (Prag));
+ Expr : Node_Id;
+ Restore_Scope : Boolean := False;
+ -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
+
begin
-- Ensure that the subprogram and its formals are visible when analyzing
-- the expression of the pragma.
if Current_Scope /= Subp_Id then
- Restore := True;
+ Restore_Scope := True;
Push_Scope (Subp_Id);
Install_Formals (Subp_Id);
end if;
@@ -18465,7 +18513,7 @@
-- Remove the subprogram from the scope stack now that the pre-analysis
-- of the precondition/postcondition is done.
- if Restore then
+ if Restore_Scope then
End_Scope;
end if;
end Analyze_Pre_Post_Condition_In_Decl_Part;
@@ -18494,6 +18542,497 @@
null;
end Analyze_Refined_Global_In_Decl_Part;
+ ----------------------------------------
+ -- Analyze_Refined_State_In_Decl_Part --
+ ----------------------------------------
+
+ procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id) is
+ Pack_Body : constant Node_Id := Parent (N);
+ Spec_Id : constant Entity_Id := Corresponding_Spec (Pack_Body);
+
+ Abstr_States : Elist_Id := No_Elist;
+ -- A list of all abstract states defined in the package declaration. The
+ -- list is used to report unrefined states.
+
+ Constituents_Seen : Elist_Id := No_Elist;
+ -- A list that contains all constituents processed so far. The list is
+ -- used to detect multiple uses of the same constituent.
+
+ Hidden_States : Elist_Id := No_Elist;
+ -- A list of all hidden states (abstract states and variables) that
+ -- appear in the package spec and body. The list is used to report
+ -- unused hidden states.
+
+ Refined_States_Seen : Elist_Id := No_Elist;
+ -- A list that contains all refined states processed so far. The list is
+ -- used to detect duplicate refinements.
+
+ procedure Analyze_Refinement_Clause (Clause : Node_Id);
+ -- Perform full analysis of a single refinement clause
+
+ function Collect_Hidden_States return Elist_Id;
+ -- Gather the entities of all hidden states that appear in the spec and
+ -- body of the related package.
+
+ procedure Report_Unrefined_States;
+ -- Emit errors for all abstract states that have not been refined by
+ -- the pragma.
+
+ procedure Report_Unused_Hidden_States;
+ -- Emit errors for all hidden states of the related package that do not
+ -- participate in a refinement.
+
+ -------------------------------
+ -- Analyze_Refinement_Clause --
+ -------------------------------
+
+ procedure Analyze_Refinement_Clause (Clause : Node_Id) is
+ Non_Null_Seen : Boolean := False;
+ Null_Seen : Boolean := False;
+ -- Flags used to detect multiple uses of null in a single clause or a
+ -- mixture of null and non-null constituents.
+
+ procedure Analyze_Constituent (Constit : Node_Id);
+ -- Perform full analysis of a single constituent
+
+ procedure Check_Matching_State
+ (State : Node_Id;
+ State_Id : Entity_Id);
+ -- Determine whether state State denoted by its name State_Id appears
+ -- in Abstr_States. Emit an error when attempting to re-refine the
+ -- state or when the state is not defined in the package declaration.
+ -- Otherwise remove the state from Abstr_States.
+
+ -------------------------
+ -- Analyze_Constituent --
+ -------------------------
+
+ procedure Analyze_Constituent (Constit : Node_Id) is
+ procedure Check_Matching_Constituent (Constit_Id : Entity_Id);
+ -- Determine whether constituent Constit denoted by its entity
+ -- Constit_Id appears in Hidden_States. Emit an error when the
+ -- constituent is not a valid hidden state of the related package
+ -- or when it is used more than once. Otherwise remove the
+ -- constituent from Hidden_States.
+
+ --------------------------------
+ -- Check_Matching_Constituent --
+ --------------------------------
+
+ procedure Check_Matching_Constituent (Constit_Id : Entity_Id) is
+ State_Elmt : Elmt_Id;
+
+ begin
+ -- Detect a duplicate use of a constituent
+
+ if Contains (Constituents_Seen, Constit_Id) then
+ Error_Msg_NE
+ ("duplicate use of constituent &", Constit, Constit_Id);
+ return;
+ end if;
+
+ -- Inspect the hidden states of the related package looking for
+ -- a match.
+
+ State_Elmt := First_Elmt (Hidden_States);
+ while Present (State_Elmt) loop
+
+ -- A valid hidden state or variable participates in a
+ -- refinement. Add the constituent to the list of processed
+ -- items to aid with the detection of duplicate constituent
+ -- use. Remove the constituent from Hidden_States to signal
+ -- that it has already been used.
+
+ if Node (State_Elmt) = Constit_Id then
+ Add_Item (Constit_Id, Constituents_Seen);
+ Remove_Elmt (Hidden_States, State_Elmt);
+
+ return;
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+
+ -- If we get here, we are refining a state that is not hidden
+ -- with respect to the related package.
+
+ Error_Msg_Name_1 := Chars (Spec_Id);
+ Error_Msg_NE
+ ("cannot use & in refinement, constituent is not a hidden "
+ & "state of package %", Constit, Constit_Id);
+ end Check_Matching_Constituent;
+
+ -- Local variables
+
+ Constit_Id : Entity_Id;
+
+ -- Start of processing for Analyze_Constituent
+
+ begin
+ -- Detect multiple uses of null in a single refinement clause or a
+ -- mixture of null and non-null constituents.
+
+ if Nkind (Constit) = N_Null then
+ if Null_Seen then
+ Error_Msg_N
+ ("multiple null constituents not allowed", Constit);
+
+ elsif Non_Null_Seen then
+ Error_Msg_N
+ ("cannot mix null and non-null constituents", Constit);
+
+ else
+ Null_Seen := True;
+ end if;
+
+ -- Non-null constituents
+
+ else
+ Non_Null_Seen := True;
+
+ if Null_Seen then
+ Error_Msg_N
+ ("cannot mix null and non-null constituents", Constit);
+ end if;
+
+ Analyze (Constit);
+
+ -- Ensure that the constituent denotes a valid state or a
+ -- whole variable.
+
+ if Is_Entity_Name (Constit) then
+ Constit_Id := Entity (Constit);
+
+ if Ekind_In (Constit_Id, E_Abstract_State, E_Variable) then
+ Check_Matching_Constituent (Constit_Id);
+ else
+ Error_Msg_NE
+ ("constituent & must denote a variable or state",
+ Constit, Constit_Id);
+ end if;
+
+ -- The constituent is illegal
+
+ else
+ Error_Msg_N ("malformed constituent", Constit);
+ end if;
+ end if;
+ end Analyze_Constituent;
+
+ --------------------------
+ -- Check_Matching_State --
+ --------------------------
+
+ procedure Check_Matching_State
+ (State : Node_Id;
+ State_Id : Entity_Id)
+ is
+ State_Elmt : Elmt_Id;
+
+ begin
+ -- Detect a duplicate refinement of a state
+
+ if Contains (Refined_States_Seen, State_Id) then
+ Error_Msg_NE
+ ("duplicate refinement of state &", State, State_Id);
+ return;
+ end if;
+
+ -- Inspect the abstract states defined in the package declaration
+ -- looking for a match.
+
+ State_Elmt := First_Elmt (Abstr_States);
+ while Present (State_Elmt) loop
+
+ -- A valid abstract state is being refined in the body. Add
+ -- the state to the list of processed refined states to aid
+ -- with the detection of duplicate refinements. Remove the
+ -- state from Abstr_States to signal that it has already been
+ -- refined.
+
+ if Node (State_Elmt) = State_Id then
+ Add_Item (State_Id, Refined_States_Seen);
+ Remove_Elmt (Abstr_States, State_Elmt);
+
+ return;
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+
+ -- If we get here, we are refining a state that is not defined in
+ -- the package declaration.
+
+ Error_Msg_Name_1 := Chars (Spec_Id);
+ Error_Msg_NE
+ ("cannot refine state, & is not defined in package %",
+ State, State_Id);
+ end Check_Matching_State;
+
+ -- Local declarations
+
+ Constit : Node_Id;
+ State : Node_Id;
+ State_Id : Entity_Id := Empty;
+
+ -- Start of processing for Analyze_Refinement_Clause
+
+ begin
+ -- Analyze the state name of a refinement clause
+
+ State := First (Choices (Clause));
+ while Present (State) loop
+ if Present (State_Id) then
+ Error_Msg_N
+ ("refinement clause cannot cover multiple states", State);
+
+ else
+ Analyze (State);
+
+ -- Ensure that the state name denotes a valid abstract state
+ -- that is defined in the spec of the related package.
+
+ if Is_Entity_Name (State) then
+ State_Id := Entity (State);
+
+ -- Catch any attempts to re-refine a state or refine a
+ -- state that is not defined in the package declaration.
+
+ if Ekind (State_Id) = E_Abstract_State then
+ Check_Matching_State (State, State_Id);
+ else
+ Error_Msg_NE
+ ("& must denote an abstract state", State, State_Id);
+ end if;
+
+ -- The state name is illegal
+
+ else
+ Error_Msg_N
+ ("malformed state name in refinement clause", State);
+ end if;
+ end if;
+
+ Next (State);
+ end loop;
+
+ -- Analyze all constituents of the refinement. Multiple constituents
+ -- appear as an aggregate.
+
+ Constit := Expression (Clause);
+
+ if Nkind (Constit) = N_Aggregate then
+ if Present (Component_Associations (Constit)) then
+ Error_Msg_N
+ ("constituents of refinement clause must appear in "
+ & "positional form", Constit);
+
+ else pragma Assert (Present (Expressions (Constit)));
+ Constit := First (Expressions (Constit));
+ while Present (Constit) loop
+ Analyze_Constituent (Constit);
+
+ Next (Constit);
+ end loop;
+ end if;
+
+ -- Various forms of a single constituent. Note that these may include
+ -- malformed constituents.
+
+ else
+ Analyze_Constituent (Constit);
+ end if;
+ end Analyze_Refinement_Clause;
+
+ ---------------------------
+ -- Collect_Hidden_States --
+ ---------------------------
+
+ function Collect_Hidden_States return Elist_Id is
+ Result : Elist_Id := No_Elist;
+
+ procedure Collect_Hidden_States_In_Decls (Decls : List_Id);
+ -- Find all hidden states that appear in declarative list Decls and
+ -- append their entities to Result.
+
+ ------------------------------------
+ -- Collect_Hidden_States_In_Decls --
+ ------------------------------------
+
+ procedure Collect_Hidden_States_In_Decls (Decls : List_Id) is
+ procedure Collect_Abstract_States (States : Elist_Id);
+ -- Copy the abstract states defined in list States to list Result
+
+ -----------------------------
+ -- Collect_Abstract_States --
+ -----------------------------
+
+ procedure Collect_Abstract_States (States : Elist_Id) is
+ State_Elmt : Elmt_Id;
+
+ begin
+ State_Elmt := First_Elmt (States);
+ while Present (State_Elmt) loop
+ Add_Item (Node (State_Elmt), Result);
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end Collect_Abstract_States;
+
+ -- Local variables
+
+ Decl : Node_Id;
+
+ -- Start of processing for Collect_Hidden_States_In_Decls
+
+ begin
+ Decl := First (Decls);
+ while Present (Decl) loop
+
+ -- Objects (non-constants) are valid hidden states
+
+ if Nkind (Decl) = N_Object_Declaration
+ and then not Constant_Present (Decl)
+ then
+ Add_Item (Defining_Entity (Decl), Result);
+
+ -- Gather the abstract states of a package along with all
+ -- hidden states in its visible declarations.
+
+ elsif Nkind (Decl) = N_Package_Declaration then
+ Collect_Abstract_States
+ (Abstract_States (Defining_Entity (Decl)));
+
+ Collect_Hidden_States_In_Decls
+ (Visible_Declarations (Specification (Decl)));
+ end if;
+
+ Next (Decl);
+ end loop;
+ end Collect_Hidden_States_In_Decls;
+
+ -- Local variables
+
+ Pack_Spec : constant Node_Id := Parent (Spec_Id);
+
+ -- Start of processing for Collect_Hidden_States
+
+ begin
+ -- Process the private declarations of the package spec and the
+ -- declarations of the body.
+
+ Collect_Hidden_States_In_Decls (Private_Declarations (Pack_Spec));
+ Collect_Hidden_States_In_Decls (Declarations (Pack_Body));
+
+ return Result;
+ end Collect_Hidden_States;
+
+ -----------------------------
+ -- Report_Unrefined_States --
+ -----------------------------
+
+ procedure Report_Unrefined_States is
+ State_Elmt : Elmt_Id;
+
+ begin
+ if Present (Abstr_States) then
+ State_Elmt := First_Elmt (Abstr_States);
+ while Present (State_Elmt) loop
+ Error_Msg_N
+ ("abstract state & must be refined", Node (State_Elmt));
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+ end Report_Unrefined_States;
+
+ ---------------------------------
+ -- Report_Unused_Hidden_States --
+ ---------------------------------
+
+ procedure Report_Unused_Hidden_States is
+ Posted : Boolean := False;
+ State_Elmt : Elmt_Id;
+ State_Id : Entity_Id;
+
+ begin
+ if Present (Hidden_States) then
+ State_Elmt := First_Elmt (Hidden_States);
+ while Present (State_Elmt) loop
+ State_Id := Node (State_Elmt);
+
+ -- Generate an error message of the form:
+
+ -- package ... has unused hidden states
+ -- abstract state ... defined at ...
+ -- variable ... defined at ...
+
+ if not Posted then
+ Posted := True;
+ Error_Msg_NE
+ ("package & has unused hidden states", N, Spec_Id);
+ end if;
+
+ Error_Msg_Sloc := Sloc (State_Id);
+
+ if Ekind (State_Id) = E_Abstract_State then
+ Error_Msg_NE ("\ abstract state & defined #", N, State_Id);
+ else
+ Error_Msg_NE ("\ variable & defined #", N, State_Id);
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+ end Report_Unused_Hidden_States;
+
+ -- Local declarations
+
+ Clauses : constant Node_Id :=
+ Expression (First (Pragma_Argument_Associations (N)));
+ Clause : Node_Id;
+
+ -- Start of processing for Analyze_Refined_State_In_Decl_Part
+
+ begin
+ Set_Analyzed (N);
+
+ -- Initialize the various lists used during analysis
+
+ Abstr_States := Clone (Abstract_States (Spec_Id));
+ Hidden_States := Collect_Hidden_States;
+
+ -- Multiple state refinements appear as an aggregate
+
+ if Nkind (Clauses) = N_Aggregate then
+ if Present (Expressions (Clauses)) then
+ Error_Msg_N
+ ("state refinements must appear as component associations",
+ Clauses);
+
+ else pragma Assert (Present (Component_Associations (Clauses)));
+ Clause := First (Component_Associations (Clauses));
+ while Present (Clause) loop
+ Analyze_Refinement_Clause (Clause);
+
+ Next (Clause);
+ end loop;
+ end if;
+
+ -- Various forms of a single state refinement. Note that these may
+ -- include malformed refinements.
+
+ else
+ Analyze_Refinement_Clause (Clauses);
+ end if;
+
+ -- Ensure that all abstract states have been refined and all hidden
+ -- states of the related package unilized in refinements.
+
+ Report_Unrefined_States;
+ Report_Unused_Hidden_States;
+ end Analyze_Refined_State_In_Decl_Part;
+
------------------------------------
-- Analyze_Test_Case_In_Decl_Part --
------------------------------------
@@ -19250,6 +19789,7 @@
Pragma_Refined_Global => -1,
Pragma_Refined_Post => -1,
Pragma_Refined_Pre => -1,
+ Pragma_Refined_State => -1,
Pragma_Relative_Deadline => -1,
Pragma_Remote_Access_Type => -1,
Pragma_Remote_Call_Interface => -1,
Index: sem_prag.ads
===================================================================
--- sem_prag.ads (revision 203365)
+++ sem_prag.ads (working copy)
@@ -77,6 +77,9 @@
procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Refined_Global
+ procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Refined_State
+
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id);
-- Perform preanalysis of pragma Test_Case that applies to a subprogram
-- declaration. Parameter N denotes the pragma, S is the entity of the
Index: elists.adb
===================================================================
--- elists.adb (revision 203342)
+++ elists.adb (working copy)
@@ -158,6 +158,34 @@
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 --
--------------
Index: elists.ads
===================================================================
--- elists.ads (revision 203342)
+++ elists.ads (working copy)
@@ -153,6 +153,10 @@
-- 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: aspects.adb
===================================================================
--- aspects.adb (revision 203365)
+++ aspects.adb (working copy)
@@ -470,6 +470,7 @@
Aspect_Refined_Global => Aspect_Refined_Global,
Aspect_Refined_Post => Aspect_Refined_Post,
Aspect_Refined_Pre => Aspect_Refined_Pre,
+ Aspect_Refined_State => Aspect_Refined_State,
Aspect_Remote_Access_Type => Aspect_Remote_Access_Type,
Aspect_Remote_Call_Interface => Aspect_Remote_Call_Interface,
Aspect_Remote_Types => Aspect_Remote_Types,
Index: aspects.ads
===================================================================
--- aspects.ads (revision 203365)
+++ aspects.ads (working copy)
@@ -115,6 +115,7 @@
Aspect_Refined_Global, -- GNAT
Aspect_Refined_Post, -- GNAT
Aspect_Refined_Pre, -- GNAT
+ Aspect_Refined_State, -- GNAT
Aspect_Relative_Deadline,
Aspect_Scalar_Storage_Order, -- GNAT
Aspect_Simple_Storage_Pool, -- GNAT
@@ -327,6 +328,7 @@
Aspect_Refined_Global => Expression,
Aspect_Refined_Post => Expression,
Aspect_Refined_Pre => Expression,
+ Aspect_Refined_State => Expression,
Aspect_Relative_Deadline => Expression,
Aspect_Scalar_Storage_Order => Expression,
Aspect_Simple_Storage_Pool => Name,
@@ -427,6 +429,7 @@
Aspect_Refined_Global => Name_Refined_Global,
Aspect_Refined_Post => Name_Refined_Post,
Aspect_Refined_Pre => Name_Refined_Pre,
+ Aspect_Refined_State => Name_Refined_State,
Aspect_Relative_Deadline => Name_Relative_Deadline,
Aspect_Remote_Access_Type => Name_Remote_Access_Type,
Aspect_Remote_Call_Interface => Name_Remote_Call_Interface,
@@ -620,6 +623,7 @@
Aspect_Read => Always_Delay,
Aspect_Refined_Depends => Always_Delay,
Aspect_Refined_Global => Always_Delay,
+ Aspect_Refined_State => Always_Delay,
Aspect_Relative_Deadline => Always_Delay,
Aspect_Remote_Access_Type => Always_Delay,
Aspect_Remote_Call_Interface => Always_Delay,
Index: par-prag.adb
===================================================================
--- par-prag.adb (revision 203365)
+++ par-prag.adb (working copy)
@@ -1254,6 +1254,7 @@
Pragma_Refined_Global |
Pragma_Refined_Post |
Pragma_Refined_Pre |
+ Pragma_Refined_State |
Pragma_Relative_Deadline |
Pragma_Remote_Access_Type |
Pragma_Remote_Call_Interface |
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 203368)
+++ sem_ch13.adb (working copy)
@@ -1883,13 +1883,46 @@
-- Abstract_State
- when Aspect_Abstract_State =>
- Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_Abstract_State);
+ when Aspect_Abstract_State => Abstract_State : declare
+ Decls : List_Id;
+ Spec : Node_Id;
+ begin
+ -- Aspect Abstract_State introduces implicit declarations
+ -- for all state abstraction entities it defines. To emulate
+ -- this behavior, insert the pragma at the beginning of the
+ -- visible declarations of the related package so that it is
+ -- analyzed immediately.
+
+ if Nkind_In (N, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Spec := Specification (N);
+ Decls := Visible_Declarations (Spec);
+
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Abstract_State);
+ Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Visible_Declarations (N, Decls);
+ end if;
+
+ Prepend_To (Decls, Aitem);
+
+ else
+ Error_Msg_NE
+ ("aspect & must apply to a package declaration",
+ Aspect, Id);
+ end if;
+
+ goto Continue;
+ end Abstract_State;
+
-- Depends
-- Aspect Depends must be delayed because it mentions names
@@ -1967,6 +2000,42 @@
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_Refined_Pre);
+ -- Refined_State
+
+ when Aspect_Refined_State => Refined_State : declare
+ Decls : List_Id;
+
+ begin
+ -- The corresponding pragma for Refined_State is inserted in
+ -- the declarations of the related package body. This action
+ -- synchronizes both the source and from-aspect versions of
+ -- the pragma.
+
+ if Nkind (N) = N_Package_Body then
+ Decls := Declarations (N);
+
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Refined_State);
+ Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Declarations (N, Decls);
+ end if;
+
+ Prepend_To (Decls, Aitem);
+
+ else
+ Error_Msg_NE
+ ("aspect & must apply to a package body", Aspect, Id);
+ end if;
+
+ goto Continue;
+ end Refined_State;
+
-- Relative_Deadline
when Aspect_Relative_Deadline =>
@@ -2411,21 +2480,6 @@
Set_From_Aspect_Specification (Aitem, True);
end if;
- -- Aspect Abstract_State introduces implicit declarations for all
- -- state abstraction entities it defines. To emulate this behavior
- -- insert the pragma at the start of the visible declarations of
- -- the related package.
-
- if Nam = Name_Abstract_State
- and then Nkind (N) = N_Package_Declaration
- then
- if No (Visible_Declarations (Specification (N))) then
- Set_Visible_Declarations (Specification (N), New_List);
- end if;
-
- Prepend (Aitem, Visible_Declarations (Specification (N)));
- goto Continue;
-
-- In the context of a compilation unit, we directly put the
-- pragma in the Pragmas_After list of the N_Compilation_Unit_Aux
-- node (no delay is required here) except for aspects on a
@@ -2434,7 +2488,7 @@
-- copy (see sem_ch12), and for package instantiations, where
-- the library unit pragmas are better handled early.
- elsif Nkind (Parent (N)) = N_Compilation_Unit
+ if Nkind (Parent (N)) = N_Compilation_Unit
and then (Present (Aitem) or else Is_Boolean_Aspect (Aspect))
then
declare
@@ -7651,6 +7705,7 @@
Aspect_Refined_Global |
Aspect_Refined_Post |
Aspect_Refined_Pre |
+ Aspect_Refined_State |
Aspect_SPARK_Mode |
Aspect_Test_Case =>
raise Program_Error;
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl (revision 203365)
+++ snames.ads-tmpl (working copy)
@@ -584,6 +584,10 @@
Name_Refined_Global : constant Name_Id := N + $; -- GNAT
Name_Refined_Post : constant Name_Id := N + $; -- GNAT
Name_Refined_Pre : constant Name_Id := N + $; -- GNAT
+
+ -- Kirchev
+
+ Name_Refined_State : constant Name_Id := N + $; -- GNAT
Name_Relative_Deadline : constant Name_Id := N + $; -- Ada 05
Name_Remote_Access_Type : constant Name_Id := N + $; -- GNAT
Name_Remote_Call_Interface : constant Name_Id := N + $;
@@ -1871,6 +1875,7 @@
Pragma_Refined_Global,
Pragma_Refined_Post,
Pragma_Refined_Pre,
+ Pragma_Refined_State,
Pragma_Relative_Deadline,
Pragma_Remote_Access_Type,
Pragma_Remote_Call_Interface,
