===================================================================
@@ -2224,9 +2224,9 @@
if Present (L) then
Context := Parent (L);
- -- Analyze aspect/pragma Initializes of a package at the end of the
- -- visible declarations as the aspect/pragma has visibility over the
- -- said region.
+ -- Analyze pragmas Initializes and Initial_Condition of a package at
+ -- the end of the visible declarations as the pragmas have visibility
+ -- over the said region.
if Nkind (Context) = N_Package_Specification
and then L = Visible_Declarations (Context)
@@ -2238,6 +2238,12 @@
Analyze_Initializes_In_Decl_Part (Prag);
end if;
+ Prag := Get_Pragma (Spec_Id, Pragma_Initial_Condition);
+
+ if Present (Prag) then
+ Analyze_Initial_Condition_In_Decl_Part (Prag);
+ end if;
+
-- 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
===================================================================
@@ -368,6 +368,11 @@
-- Given an arbitrary entity, traverse the scope chain looking for the
-- first enclosing function. Return Empty if no function was found.
+ procedure Expand_Pragma_Initial_Condition (N : Node_Id);
+ -- Subsidiary to the expansion of package specs and bodies. Generate a
+ -- runtime check needed to verify the assumption introduced by pragma
+ -- Initial_Condition. N denotes the package spec or body.
+
function Make_Call
(Loc : Source_Ptr;
Proc_Id : Entity_Id;
@@ -3959,6 +3964,15 @@
end if;
Build_Task_Activation_Call (N);
+
+ -- When the package is subject to pragma Initial_Condition, the
+ -- assertion expression must be verified at the end of the body
+ -- statements.
+
+ if Present (Get_Pragma (Spec_Ent, Pragma_Initial_Condition)) then
+ Expand_Pragma_Initial_Condition (N);
+ end if;
+
Pop_Scope;
end if;
@@ -4053,10 +4067,9 @@
if No_Body then
Push_Scope (Id);
+ -- Generate RACW subprogram bodies
+
if Has_RACW (Id) then
-
- -- Generate RACW subprogram bodies
-
Decls := Private_Declarations (Spec);
if No (Decls) then
@@ -4072,11 +4085,19 @@
Analyze_List (Decls);
end if;
+ -- Generate task activation call as last step of elaboration
+
if Present (Activation_Chain_Entity (N)) then
+ Build_Task_Activation_Call (N);
+ end if;
- -- Generate task activation call as last step of elaboration
+ -- When the package is subject to pragma Initial_Condition and lacks
+ -- a body, the assertion expression must be verified at the end of
+ -- the visible declarations. Otherwise the check is performed at the
+ -- end of the body statements (see Expand_N_Package_Body).
- Build_Task_Activation_Call (N);
+ if Present (Get_Pragma (Id, Pragma_Initial_Condition)) then
+ Expand_Pragma_Initial_Condition (N);
end if;
Pop_Scope;
@@ -4114,6 +4135,88 @@
end if;
end Expand_N_Package_Declaration;
+ -------------------------------------
+ -- Expand_Pragma_Initial_Condition --
+ -------------------------------------
+
+ procedure Expand_Pragma_Initial_Condition (N : Node_Id) is
+ Loc : constant Source_Ptr := Sloc (N);
+ Check : Node_Id;
+ Expr : Node_Id;
+ Init_Cond : Node_Id;
+ List : List_Id;
+ Pack_Id : Entity_Id;
+
+ begin
+ if Nkind (N) = N_Package_Body then
+ Pack_Id := Corresponding_Spec (N);
+
+ if Present (Handled_Statement_Sequence (N)) then
+ List := Statements (Handled_Statement_Sequence (N));
+
+ -- The package body lacks statements, create an empty list
+
+ else
+ List := New_List;
+
+ Set_Handled_Statement_Sequence (N,
+ Make_Handled_Sequence_Of_Statements (Loc, Statements => List));
+ end if;
+
+ elsif Nkind (N) = N_Package_Declaration then
+ Pack_Id := Defining_Entity (N);
+
+ if Present (Visible_Declarations (Specification (N))) then
+ List := Visible_Declarations (Specification (N));
+
+ -- The package lacks visible declarations, create an empty list
+
+ else
+ List := New_List;
+
+ Set_Visible_Declarations (Specification (N), List);
+ end if;
+
+ -- This routine should not be used on anything other than packages
+
+ else
+ raise Program_Error;
+ end if;
+
+ Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
+
+ -- The caller should check whether the package is subject to pragma
+ -- Initial_Condition.
+
+ pragma Assert (Present (Init_Cond));
+
+ Expr :=
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (Init_Cond)));
+
+ -- The assertion expression was found to be illegal, do not generate the
+ -- runtime check as it will repeat the illegality.
+
+ if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
+ return;
+ end if;
+
+ -- Generate:
+ -- pragma Check (Initial_Condition, <Expr>);
+
+ Check :=
+ Make_Pragma (Loc,
+ Chars => Name_Check,
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_Identifier (Loc, Name_Initial_Condition)),
+
+ Make_Pragma_Argument_Association (Loc,
+ Expression => New_Copy_Tree (Expr))));
+
+ Append_To (List, Check);
+ Analyze (Check);
+ end Expand_Pragma_Initial_Condition;
+
-----------------------------
-- Find_Node_To_Be_Wrapped --
-----------------------------
===================================================================
@@ -7198,6 +7198,7 @@
-- Abstract_States
-- Depends
-- Global
+ -- Initial_Condition
-- Initializes
-- Refined_Depends
-- Refined_Global
===================================================================
@@ -6300,18 +6300,19 @@
function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is
Is_CDG : constant Boolean :=
- Id = Pragma_Abstract_State or else
- Id = Pragma_Depends or else
- Id = Pragma_Global or else
- Id = Pragma_Initializes or else
- Id = Pragma_Refined_Depends or else
- Id = Pragma_Refined_Global or else
+ Id = Pragma_Abstract_State or else
+ Id = Pragma_Depends or else
+ Id = Pragma_Global or else
+ Id = Pragma_Initial_Condition or else
+ Id = Pragma_Initializes or else
+ Id = Pragma_Refined_Depends or else
+ Id = Pragma_Refined_Global or else
Id = Pragma_Refined_State;
Is_CTC : constant Boolean :=
- Id = Pragma_Contract_Cases or else
+ Id = Pragma_Contract_Cases or else
Id = Pragma_Test_Case;
Is_PPC : constant Boolean :=
- Id = Pragma_Precondition or else
+ Id = Pragma_Precondition or else
Id = Pragma_Postcondition;
In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC;
===================================================================
@@ -7442,6 +7442,8 @@
-- Contract_Cases
-- Depends
-- Global
+ -- Initial_Condition
+ -- Initializes
-- Precondition
-- Postcondition
-- Refined_Depends
===================================================================
@@ -911,9 +911,9 @@
-- as input. OUT parameters are valid inputs only when their type
-- is unconstrained or tagged as their discriminants, array bouns
-- or tags can be read. In general, states and variables are
- -- considered to have mode IN OUT unless they are moded by pragma
- -- [Refined_]Global. In that case, the item must appear in an
- -- input global list.
+ -- considered to have mode IN OUT unless they are classified by
+ -- pragma [Refined_]Global. In that case, the item must appear in
+ -- an input global list.
if (Ekind (Item_Id) = E_Out_Parameter
and then not Is_Unconstrained_Or_Tagged_Item (Item_Id))
@@ -1964,6 +1964,194 @@
end if;
end Analyze_Global_In_Decl_Part;
+ --------------------------------------------
+ -- Analyze_Initial_Condition_In_Decl_Part --
+ --------------------------------------------
+
+ procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is
+ Pack_Id : constant Entity_Id := Defining_Entity (Parent (Parent (N)));
+ Prag_Init : constant Node_Id :=
+ Get_Pragma (Pack_Id, Pragma_Initializes);
+ -- The related pragma Initializes
+
+ Vars : Elist_Id := No_Elist;
+ -- A list of all variables declared in pragma Initializes
+
+ procedure Collect_Variables;
+ -- Inspect the initialization list of pragma Initializes and collect the
+ -- entities of all variables declared within the related package.
+
+ function Match_Variable (N : Node_Id) return Traverse_Result;
+ -- Determine whether arbitrary node N denotes a variable declared in the
+ -- visible declarations of the related package.
+
+ procedure Report_Unused_Variables;
+ -- Emit errors for all variables found in list Vars
+
+ -----------------------
+ -- Collect_Variables --
+ -----------------------
+
+ procedure Collect_Variables is
+ procedure Collect_Variable (Item : Node_Id);
+ -- Determine whether Item denotes a variable that appears in the
+ -- related package and if it does, add it to list Vars.
+
+ ----------------------
+ -- Collect_Variable --
+ ----------------------
+
+ procedure Collect_Variable (Item : Node_Id) is
+ Item_Id : Entity_Id;
+
+ begin
+ if Is_Entity_Name (Item) and then Present (Entity (Item)) then
+ Item_Id := Entity (Item);
+
+ -- The item is a variable declared in the related package
+
+ if Ekind (Item_Id) = E_Variable
+ and then Scope (Item_Id) = Pack_Id
+ then
+ Add_Item (Item_Id, Vars);
+ end if;
+ end if;
+ end Collect_Variable;
+
+ -- Local variables
+
+ Inits : constant Node_Id :=
+ Get_Pragma_Arg
+ (First (Pragma_Argument_Associations (Prag_Init)));
+ Init : Node_Id;
+
+ -- Start of processing for Collect_Variables
+
+ begin
+ -- Multiple initialization items appear as an aggregate
+
+ if Nkind (Inits) = N_Aggregate
+ and then Present (Expressions (Inits))
+ then
+ Init := First (Expressions (Inits));
+ while Present (Init) loop
+ Collect_Variable (Init);
+
+ Next (Init);
+ end loop;
+
+ -- Single initialization item
+
+ else
+ Collect_Variable (Inits);
+ end if;
+ end Collect_Variables;
+
+ --------------------
+ -- Match_Variable --
+ --------------------
+
+ function Match_Variable (N : Node_Id) return Traverse_Result is
+ Var_Id : Entity_Id;
+
+ begin
+ -- Find a variable declared within the related package and try to
+ -- remove it from the list of collected variables found in pragma
+ -- Initializes.
+
+ if Is_Entity_Name (N)
+ and then Present (Entity (N))
+ then
+ Var_Id := Entity (N);
+
+ if Ekind (Var_Id) = E_Variable
+ and then Scope (Var_Id) = Pack_Id
+ then
+ Remove (Vars, Var_Id);
+ end if;
+ end if;
+
+ return OK;
+ end Match_Variable;
+
+ procedure Match_Variables is new Traverse_Proc (Match_Variable);
+
+ -----------------------------
+ -- Report_Unused_Variables --
+ -----------------------------
+
+ procedure Report_Unused_Variables is
+ Posted : Boolean := False;
+ Var_Elmt : Elmt_Id;
+ Var_Id : Entity_Id;
+
+ begin
+ if Present (Vars) then
+ Var_Elmt := First_Elmt (Vars);
+ while Present (Var_Elmt) loop
+ Var_Id := Node (Var_Elmt);
+
+ if not Posted then
+ Posted := True;
+ Error_Msg_Name_1 := Name_Initial_Condition;
+ Error_Msg_N
+ ("expression of % must mention the following variables",
+ N);
+ end if;
+
+ Error_Msg_Sloc := Sloc (Var_Id);
+ Error_Msg_NE ("\ & declared #", N, Var_Id);
+
+ Next_Elmt (Var_Elmt);
+ end loop;
+ end if;
+ end Report_Unused_Variables;
+
+ Expr : constant Node_Id :=
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Errors : constant Nat := Serious_Errors_Detected;
+
+ -- Start of processing for Analyze_Initial_Condition_In_Decl_Part
+
+ begin
+ Set_Analyzed (N);
+
+ -- Pragma Initial_Condition depends on the names enumerated in pragma
+ -- Initializes. Without those, the analysis cannot take place.
+
+ if No (Prag_Init) then
+ Error_Msg_Name_1 := Name_Initial_Condition;
+ Error_Msg_Name_2 := Name_Initializes;
+
+ Error_Msg_N ("% requires the presence of aspect or pragma %", N);
+ return;
+ end if;
+
+ -- The expression is preanalyzed because it has not been moved to its
+ -- final place yet. A direct analysis may generate sife effects and this
+ -- is not desired at this point.
+
+ Preanalyze_And_Resolve (Expr, Standard_Boolean);
+
+ -- Perform variable matching only when the expression is legal
+
+ if Serious_Errors_Detected = Errors then
+ Collect_Variables;
+
+ -- Verify that all variables mentioned in pragma Initializes are used
+ -- in the expression of pragma Initial_Condition.
+
+ Match_Variables (Expr);
+ end if;
+
+ -- Emit errors for all variables that should participate in the
+ -- expression of pragma Initial_Condition.
+
+ if Serious_Errors_Detected = Errors then
+ Report_Unused_Variables;
+ end if;
+ end Analyze_Initial_Condition_In_Decl_Part;
+
--------------------------------------
-- Analyze_Initializes_In_Decl_Part --
--------------------------------------
@@ -2451,10 +2639,10 @@
-- UU_Typ is the related Unchecked_Union type. Flag In_Variant_Part
-- should be set when Comp comes from a record variant.
- procedure Check_Declaration_Order (States : Node_Id; Inits : Node_Id);
- -- Subsidiary routine to the analysis of pragmas Abstract_State and
- -- Initializes. Determine whether pragma Abstract_State denoted by
- -- States is defined earlier than pragma Initializes denoted by Inits.
+ procedure Check_Declaration_Order (First : Node_Id; Second : Node_Id);
+ -- Subsidiary routine to the analysis of pragmas Abstract_State,
+ -- Initial_Condition and Initializes. Determine whether pragma First
+ -- appears before pragma Second. If this is not the case, emit an error.
procedure Check_Duplicate_Pragma (E : Entity_Id);
-- Check if a rep item of the same name as the current pragma is already
@@ -3433,7 +3621,7 @@
-- Check_Declaration_Order --
-----------------------------
- procedure Check_Declaration_Order (States : Node_Id; Inits : Node_Id) is
+ procedure Check_Declaration_Order (First : Node_Id; Second : Node_Id) is
procedure Check_Aspect_Specification_Order;
-- Inspect the aspect specifications of the context to determine the
-- proper order.
@@ -3443,33 +3631,34 @@
--------------------------------------
procedure Check_Aspect_Specification_Order is
- Asp_I : constant Node_Id := Corresponding_Aspect (Inits);
- Asp_S : constant Node_Id := Corresponding_Aspect (States);
- Asp : Node_Id;
+ Asp_First : constant Node_Id := Corresponding_Aspect (First);
+ Asp_Second : constant Node_Id := Corresponding_Aspect (Second);
+ Asp : Node_Id;
- States_Seen : Boolean := False;
-
begin
-- Both aspects must be part of the same aspect specification list
- pragma Assert (List_Containing (Asp_I) = List_Containing (Asp_S));
+ pragma Assert
+ (List_Containing (Asp_First) = List_Containing (Asp_Second));
- Asp := First (List_Containing (Asp_I));
+ -- Try to reach Second starting from First in a left to right
+ -- traversal of the aspect specifications.
+
+ Asp := Next (Asp_First);
while Present (Asp) loop
- if Get_Aspect_Id (Asp) = Aspect_Abstract_State then
- States_Seen := True;
- elsif Get_Aspect_Id (Asp) = Aspect_Initializes then
- if not States_Seen then
- Error_Msg_N
- ("aspect % must come before aspect %", States);
- end if;
+ -- The order is ok, First is followed by Second
- exit;
+ if Asp = Asp_Second then
+ return;
end if;
Next (Asp);
end loop;
+
+ -- If we get here, then the aspects are out of order
+
+ Error_Msg_N ("aspect % cannot come after aspect %", First);
end Check_Aspect_Specification_Order;
-- Local variables
@@ -3481,44 +3670,41 @@
begin
-- Cannot check the order if one of the pragmas is missing
- if No (States) or else No (Inits) then
+ if No (First) or else No (Second) then
return;
end if;
-- Set up the error names in case the order is incorrect
- Error_Msg_Name_1 := Name_Abstract_State;
- Error_Msg_Name_2 := Name_Initializes;
+ Error_Msg_Name_1 := Pragma_Name (First);
+ Error_Msg_Name_2 := Pragma_Name (Second);
- if From_Aspect_Specification (States) then
+ if From_Aspect_Specification (First) then
-- Both pragmas are actually aspects, check their declaration
-- order in the associated aspect specification list. Otherwise
- -- States is an aspect and Inits a source pragma.
+ -- First is an aspect and Second a source pragma.
- if From_Aspect_Specification (Inits) then
+ if From_Aspect_Specification (Second) then
Check_Aspect_Specification_Order;
end if;
-- Abstract_States is a source pragma
else
- if From_Aspect_Specification (Inits) then
- Error_Msg_N ("pragma % cannot come after aspect %", States);
+ if From_Aspect_Specification (Second) then
+ Error_Msg_N ("pragma % cannot come after aspect %", First);
- -- Both pragmas are source constructs. Try to reach States from
- -- Inits by traversing the declarations backwards.
+ -- Both pragmas are source constructs. Try to reach First from
+ -- Second by traversing the declarations backwards.
else
- Stmt := Prev (Inits);
+ Stmt := Prev (Second);
while Present (Stmt) loop
- -- The order is ok, Abstract_States is first followed by
- -- Initializes.
+ -- The order is ok, First is followed by Second
- if Nkind (Stmt) = N_Pragma
- and then Pragma_Name (Stmt) = Name_Abstract_State
- then
+ if Stmt = First then
return;
end if;
@@ -3527,7 +3713,7 @@
-- If we get here, then the pragmas are out of order
- Error_Msg_N ("pragma % cannot come after pragma %", States);
+ Error_Msg_N ("pragma % cannot come after pragma %", First);
end if;
end if;
end Check_Declaration_Order;
@@ -9318,8 +9504,8 @@
-- Initializes.
Check_Declaration_Order
- (States => N,
- Inits => Get_Pragma (Pack_Id, Pragma_Initializes));
+ (First => N,
+ Second => Get_Pragma (Pack_Id, Pragma_Initializes));
State := Expression (Arg1);
@@ -9732,6 +9918,7 @@
-- Assume |
-- Contract_Cases |
-- Debug |
+ -- Initial_Condition |
-- Loop_Invariant |
-- Loop_Variant |
-- Postcondition |
@@ -13380,6 +13567,80 @@
end if;
end Independent_Components;
+ -----------------------
+ -- Initial_Condition --
+ -----------------------
+
+ -- pragma Initial_Condition (boolean_EXPRESSION);
+
+ when Pragma_Initial_Condition => Initial_Condition : declare
+ Context : constant Node_Id := Parent (Parent (N));
+ Pack_Id : Entity_Id;
+ Stmt : Node_Id;
+
+ begin
+ GNAT_Pragma;
+ S14_Pragma;
+ Check_Arg_Count (1);
+
+ -- Ensure the proper placement of the pragma. Initial_Condition
+ -- must be associated with a package declaration.
+
+ if not Nkind_In (Context, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Stmt := Prev (N);
+ while Present (Stmt) loop
+
+ -- Skip prior pragmas, but check for duplicates
+
+ if Nkind (Stmt) = N_Pragma then
+ if Pragma_Name (Stmt) = Pname then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_Sloc := Sloc (Stmt);
+ Error_Msg_N ("pragma % duplicates pragma declared #", N);
+ end if;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Stmt) then
+ null;
+
+ -- The pragma does not apply to a legal construct, issue an
+ -- error and stop the analysis.
+
+ else
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Stmt := Prev (Stmt);
+ end loop;
+
+ -- The pragma must be analyzed at the end of the visible
+ -- declarations of the related package. Save the pragma for later
+ -- (see Analyze_Initial_Condition_In_Decl_Part) by adding it to
+ -- the contract of the package.
+
+ Pack_Id := Defining_Entity (Context);
+ Add_Contract_Item (N, Pack_Id);
+
+ -- Verify the declaration order of pragma Initial_Condition with
+ -- respect to pragmas Abstract_State and Initializes.
+
+ Check_Declaration_Order
+ (First => Get_Pragma (Pack_Id, Pragma_Abstract_State),
+ Second => N);
+
+ Check_Declaration_Order
+ (First => Get_Pragma (Pack_Id, Pragma_Initializes),
+ Second => N);
+ end Initial_Condition;
+
------------------------
-- Initialize_Scalars --
------------------------
@@ -13461,8 +13722,8 @@
elsif not Comes_From_Source (Stmt) then
null;
- -- The pragma does not apply to a legal construct, issue an
- -- error and stop the analysis.
+ -- The pragma does not apply to a legal construct, issue an
+ -- error and stop the analysis.
else
Pragma_Misplaced;
@@ -13484,8 +13745,8 @@
-- Initializes.
Check_Declaration_Order
- (States => Get_Pragma (Pack_Id, Pragma_Abstract_State),
- Inits => N);
+ (First => Get_Pragma (Pack_Id, Pragma_Abstract_State),
+ Second => N);
end Initializes;
------------
@@ -16979,8 +17240,8 @@
elsif not Comes_From_Source (Stmt) then
null;
- -- The pragma does not apply to a legal construct, issue an
- -- error and stop the analysis.
+ -- The pragma does not apply to a legal construct, issue an
+ -- error and stop the analysis.
else
Pragma_Misplaced;
@@ -22429,6 +22690,7 @@
Pragma_Import_Valued_Procedure => 0,
Pragma_Independent => 0,
Pragma_Independent_Components => 0,
+ Pragma_Initial_Condition => -1,
Pragma_Initialize_Scalars => -1,
Pragma_Initializes => -1,
Pragma_Inline => 0,
@@ -22822,6 +23084,7 @@
Name_Assume |
Name_Contract_Cases |
Name_Debug |
+ Name_Initial_Condition |
Name_Invariant |
Name_uInvariant |
Name_Loop_Invariant |
===================================================================
@@ -64,6 +64,9 @@
-- Perform full analysis of delayed pragma Global. This routine is also
-- capable of performing basic analysis of pragma Refind_Global.
+ procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Initial_Condition
+
procedure Analyze_Initializes_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Initializes
===================================================================
@@ -229,10 +229,14 @@
-- Contract items related to [generic] packages. The applicable pragmas
-- are:
-- Abstract_States
+ -- Initial_Condition
-- Initializes
if Ekind_In (Id, E_Generic_Package, E_Package) then
- if Nam_In (Nam, Name_Abstract_State, Name_Initializes) then
+ if Nam_In (Nam, Name_Abstract_State,
+ Name_Initial_Condition,
+ Name_Initializes)
+ then
Set_Next_Pragma (Prag, Classifications (Items));
Set_Classifications (Items, Prag);
===================================================================
@@ -50,6 +50,7 @@
-- Contract_Cases
-- Depends
-- Global
+ -- Initial_Condition
-- Initializes
-- Postcondition
-- Precondition
===================================================================
@@ -440,6 +440,7 @@
Aspect_Independent_Components => Aspect_Independent_Components,
Aspect_Inline => Aspect_Inline,
Aspect_Inline_Always => Aspect_Inline,
+ Aspect_Initial_Condition => Aspect_Initial_Condition,
Aspect_Initializes => Aspect_Initializes,
Aspect_Input => Aspect_Input,
Aspect_Interrupt_Handler => Aspect_Interrupt_Handler,
===================================================================
@@ -96,6 +96,7 @@
Aspect_External_Tag,
Aspect_Global, -- GNAT
Aspect_Implicit_Dereference,
+ Aspect_Initial_Condition, -- GNAT
Aspect_Initializes, -- GNAT
Aspect_Input,
Aspect_Interrupt_Priority,
@@ -310,6 +311,7 @@
Aspect_External_Tag => Expression,
Aspect_Global => Expression,
Aspect_Implicit_Dereference => Name,
+ Aspect_Initial_Condition => Expression,
Aspect_Initializes => Expression,
Aspect_Input => Name,
Aspect_Interrupt_Priority => Expression,
@@ -400,6 +402,7 @@
Aspect_Independent_Components => Name_Independent_Components,
Aspect_Inline => Name_Inline,
Aspect_Inline_Always => Name_Inline_Always,
+ Aspect_Initial_Condition => Name_Initial_Condition,
Aspect_Initializes => Name_Initializes,
Aspect_Input => Name_Input,
Aspect_Interrupt_Handler => Name_Interrupt_Handler,
@@ -600,6 +603,7 @@
Aspect_Independent_Components => Always_Delay,
Aspect_Inline => Always_Delay,
Aspect_Inline_Always => Always_Delay,
+ Aspect_Initial_Condition => Always_Delay,
Aspect_Initializes => Always_Delay,
Aspect_Input => Always_Delay,
Aspect_Interrupt_Handler => Always_Delay,
===================================================================
@@ -1185,6 +1185,7 @@
Pragma_Import_Valued_Procedure |
Pragma_Independent |
Pragma_Independent_Components |
+ Pragma_Initial_Condition |
Pragma_Initialize_Scalars |
Pragma_Initializes |
Pragma_Inline |
===================================================================
@@ -2053,6 +2053,45 @@
Insert_Delayed_Pragma (Aitem);
goto Continue;
+ -- Initial_Condition
+
+ -- Aspect Initial_Condition covers the visible declarations of
+ -- a package and all hidden states through functions. As such,
+ -- it must be evaluated at the end of the said declarations.
+
+ when Aspect_Initial_Condition => Initial_Condition : declare
+ Decls : List_Id;
+
+ begin
+ if Nkind_In (N, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Decls := Visible_Declarations (Specification (N));
+
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name =>
+ Name_Initial_Condition);
+ 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 Initial_Condition;
+
-- Initializes
-- Aspect Initializes coverts the visible declarations of a
@@ -7849,6 +7888,7 @@
Aspect_Dimension |
Aspect_Dimension_System |
Aspect_Implicit_Dereference |
+ Aspect_Initial_Condition |
Aspect_Initializes |
Aspect_Post |
Aspect_Postcondition |
===================================================================
@@ -509,6 +509,7 @@
Name_Import_Valued_Procedure : constant Name_Id := N + $; -- GNAT
Name_Independent : constant Name_Id := N + $; -- Ada 12
Name_Independent_Components : constant Name_Id := N + $; -- Ada 12
+ Name_Initial_Condition : constant Name_Id := N + $; -- GNAT
Name_Initializes : constant Name_Id := N + $; -- GNAT
Name_Inline : constant Name_Id := N + $;
Name_Inline_Always : constant Name_Id := N + $; -- GNAT
@@ -1829,6 +1830,7 @@
Pragma_Import_Valued_Procedure,
Pragma_Independent,
Pragma_Independent_Components,
+ Pragma_Initial_Condition,
Pragma_Initializes,
Pragma_Inline,
Pragma_Inline_Always,
This patch provides the initial implementation of aspect/pragma Initial_Condition. This construct is intended for formal verification proofs. The construct has the following syntax: pragma Initial_Condition (boolean_EXPRESSION); The construct has the following semantic rules: The Initial_Condition aspect is introduced by an aspect_specification where the aspect_mark is Initial_Condition and the aspect_definition shall be a boolean expression. An Initial_Condition aspect shall only be placed in an aspect_specification of a package_specification. Each variable or state abstraction denoted in an Initial_Condition aspect of a package Q which is declared immediately within the visible part of Q shall be initialized during the elaboration of Q and be denoted by a name of an initialization_item of the Initializes aspect of Q. An Initial_Condition aspect is a sort of postcondition for the elaboration of both the specification and body of a package. If present on a package, then its Boolean_expression defines properties (a predicate) of the state of the package which can be assumed to be true immediately following the elaboration of the package. [The expression of the Initial_Condition cannot denote a state abstraction. This means that to express properties of hidden state, functions declared in the visible part acting on the state abstractions of the package must be used.] With respect to dynamic semantics, specifying a given expression as the Initial_Condition aspect of a package is equivalent to specifying that expression as the argument of an Assert pragma occurring at the end of the (possibly implicit) statement list of the (possibly implicit) body of the package. [This equivalence includes all interactions with pragma Assertion_Policy. This equivalence does not extend to matters of static semantics, such as name resolution.] An Initial_Condition expression does not cause freezing until the point where it is evaluated [, at which point everything that it might freeze has already been frozen]. ------------ -- Source -- ------------ -- semantics.ads package Semantics with Abstract_State => State, Initializes => (State, Var_1, Var_2), Initial_Condition => (Var_1 = 1 and then Var_2 = 0) is Var_1 : Integer; Var_2 : Integer; package Error_1 with Initial_Condition => (Var_3 > 0) -- no Initializes is Var_3 : Integer; end Error_1; package Error_2 with Initializes => (Var_4, Var_5), Initial_Condition => (Var_4 = 0) -- Var_5 missing is Var_4 : Integer; Var_5 : Integer; end Error_2; end Semantics; -- exec_body_ok2.ads package Exec_Body_OK2 with Initializes => Var, Initial_Condition => (Var = 123) is Var : Integer := 0; procedure Dummy; end Exec_Body_OK2; -- exec_body_ok2.adb package body Exec_Body_OK2 is procedure Dummy is begin null; end Dummy; begin Var := 123; end Exec_Body_OK2; -- runtime_ok.adb with Exec_Body_OK2; procedure Runtime_OK is begin null; end Runtime_OK; -- exec_spec_error.ads package Exec_Spec_Error with Initializes => Var, Initial_Condition => (Var = 123) is Var : Integer := 0; -- not 123 end Exec_Spec_Error; -- runtime_error2.adb with Exec_Spec_Error; procedure Runtime_Error2 is begin null; end Runtime_Error2; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnatd.V semantics.ads $ gnatmake -q -gnata -gnatd.V runtime_ok.adb $ gnatmake -q -gnata -gnatd.V runtime_error2.adb $ ./runtime_ok $ ./runtime_error2.adb semantics.ads:10:11: "Initial_Condition" requires the presence of aspect or pragma "Initializes" semantics.ads:17:11: expression of "Initial_Condition" must mention the following variables semantics.ads:17:11: "Var_5" declared at line 20 raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : Initial_Condition failed at exec_spec_error.ads:3 Tested on x86_64-pc-linux-gnu, committed on trunk 2013-10-14 Hristian Kirtchev <kirtchev@adacore.com> * aspects.adb: Add an entry in table Canonical_Aspect for Initial_Condition. * aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument, Aspect_Names and Aspect_Delay for Initial_Condition. * einfo.adb (Get_Pragma): Include pragma Initial_Condition to categorization pragmas. * einfo.ads (Get_Pragma): Update comment on usage. * exp_ch7.adb (Expand_N_Package_Body): Add a runtime check to verify the assertion introduced by pragma Initial_Condition. (Expand_N_Package_Declaration): Add a runtime check to verify the assertion introduced by pragma Initial_Condition. (Expand_Pragma_Initial_Condition): New routine. * par-prag: Include pragma Initial_Condition to the list of pragmas that do not require special processing by the parser. * sem_ch3.adb (Analyze_Declarations): Analyze pragma Initial_Condition at the end of the visible declarations. * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing for aspect Initial_Condition. (Check_Aspect_At_Freeze_Point): Aspect Initial_Condition does not need inspection at freezing. * sem_prag.adb (Analyze_Initial_Condition_In_Decl_Part): New routine. (Analyze_Pragma): Update all calls to Check_Declaration_Order. Add processing for pragma Initial_Condition. Initial_Condition is now a valid assertion kind. Add an entry in table Sig_Flags for Initial_Condition. (Check_Declaration_Order): Reimplemented to handle arbitrary pragmas. (Is_Valid_Assertion_Kind): Add an entry for Initial_Condition. * sem_pag.ads (Analyze_Initial_Condition_In_Decl_Part): New routine. * sem_util.adb (Add_Contract_Item): Pragma Initial_Condition can now be associated with a package spec. * sem_util.ads (Add_Contract_Item): Update comment on usage. * sinfo.ads: Update the documentation of node N_Contract * snames.ads-tmpl: Add new predefined name Initial_Condition. Add new pragma id for Initial_Condition.