===================================================================
@@ -1596,85 +1596,12 @@
Subunit_Name : constant Unit_Name_Type := Get_Unit_Name (N);
Unum : Unit_Number_Type;
- procedure Move_Stub_Pragmas_To_Body (Bod : Node_Id);
- -- Relocate all pragmas that apply to a subprogram body stub to the
- -- declarations of proper body Bod.
- -- Should we do this for the reamining body stub kinds???
-
procedure Optional_Subunit;
-- This procedure is called when the main unit is a stub, or when we
-- are not generating code. In such a case, we analyze the subunit if
-- present, which is user-friendly and in fact required for ASIS, but
-- we don't complain if the subunit is missing.
- -------------------------------
- -- Move_Stub_Pragmas_To_Body --
- -------------------------------
-
- procedure Move_Stub_Pragmas_To_Body (Bod : Node_Id) is
- procedure Move_Pragma (Prag : Node_Id);
- -- Relocate one pragma to the declarations of Bod
-
- -----------------
- -- Move_Pragma --
- -----------------
-
- procedure Move_Pragma (Prag : Node_Id) is
- Decls : List_Id := Declarations (Bod);
-
- begin
- if No (Decls) then
- Decls := New_List;
- Set_Declarations (Bod, Decls);
- end if;
-
- -- Unhook the pragma from its current list
-
- Remove (Prag);
- Prepend (Prag, Decls);
- end Move_Pragma;
-
- -- Local variables
-
- Next_Stmt : Node_Id;
- Stmt : Node_Id;
-
- -- Start of processing for Move_Stub_Pragmas_To_Body
-
- begin
- pragma Assert (Nkind (N) = N_Subprogram_Body_Stub);
-
- -- Perform a bit of a lookahead - peek at any subsequent source
- -- pragmas while skipping internally generated code.
-
- Stmt := Next (N);
- while Present (Stmt) loop
- Next_Stmt := Next (Stmt);
-
- -- Move a source pragma that applies to a subprogram stub to the
- -- declarations of the proper body.
-
- if Comes_From_Source (Stmt)
- and then Nkind (Stmt) = N_Pragma
- and then Pragma_On_Stub_OK (Get_Pragma_Id (Stmt))
- then
- Move_Pragma (Stmt);
-
- -- Skip internally generated code
-
- elsif not Comes_From_Source (Stmt) then
- null;
-
- -- No valid pragmas are available for relocation
-
- else
- exit;
- end if;
-
- Stmt := Next_Stmt;
- end loop;
- end Move_Stub_Pragmas_To_Body;
-
----------------------
-- Optional_Subunit --
----------------------
@@ -1932,11 +1859,11 @@
Move_Or_Merge_Aspects (From => N, To => Prop_Body);
- -- Propagate all source pragmas associated with a
- -- subprogram body stub to the proper body.
+ -- Move all source pragmas that follow the body stub and
+ -- apply to it to the declarations of the proper body.
if Nkind (N) = N_Subprogram_Body_Stub then
- Move_Stub_Pragmas_To_Body (Prop_Body);
+ Relocate_Pragmas_To_Body (N, Target_Body => Prop_Body);
end if;
-- Analyze the unit if semantics active
===================================================================
@@ -1922,6 +1922,16 @@
-- 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
+ (Body_Decl : out Node_Id;
+ Spec_Id : out Entity_Id;
+ Legal : out Boolean);
+ -- Subsidiary routine to the analysis of pragmas Refined_Pre and
+ -- Refined_Post. Body_Decl is the declaration of the subprogram body
+ -- [stub] subject to the pragma. Spec_Id is the corresponding spec of
+ -- the subprogram body [stub]. Flag Legal denotes whether the pragma
+ -- passes all legality rules.
+
procedure Check_Ada_83_Warning;
-- Issues a warning message for the current pragma if operating in Ada
-- 83 mode (used for language pragmas that are not a standard part of
@@ -2448,6 +2458,129 @@
end if;
end Ada_2012_Pragma;
+ ------------------------------
+ -- Analyze_Refined_Pre_Post --
+ ------------------------------
+
+ procedure Analyze_Refined_Pre_Post
+ (Body_Decl : out Node_Id;
+ Spec_Id : out Entity_Id;
+ Legal : out Boolean)
+ is
+ Pack_Spec : Node_Id;
+ Spec_Decl : Node_Id;
+ Stmt : Node_Id;
+
+ begin
+ -- Assume that the pragma is illegal
+
+ Body_Decl := Parent (N);
+ Spec_Id := Empty;
+ Legal := False;
+
+ GNAT_Pragma;
+ Check_Arg_Count (1);
+ Check_No_Identifiers;
+
+ -- Verify the placement of the pragma and check for duplicates
+
+ 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;
+
+ -- Emit an error when the pragma applies to an expression function
+ -- that does not act as a completion.
+
+ elsif Nkind (Stmt) = N_Subprogram_Declaration
+ and then Nkind (Original_Node (Stmt)) = N_Expression_Function
+ and then not
+ Has_Completion (Defining_Unit_Name (Specification (Stmt)))
+ then
+ Error_Pragma
+ ("pragma % cannot apply to a stand alone expression "
+ & "function");
+ return;
+
+ -- The pragma applies to a subprogram body stub
+
+ elsif Nkind (Stmt) = N_Subprogram_Body_Stub then
+ Body_Decl := Stmt;
+ exit;
+
+ -- 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;
+
+ -- Pragma Refined_Pre/Post must apply to a subprogram body [stub]
+
+ if not Nkind_In (Body_Decl, N_Subprogram_Body,
+ N_Subprogram_Body_Stub)
+ then
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ -- The body [stub] must not act as a spec, in other words it has to
+ -- be paired with a corresponding spec.
+
+ if Nkind (Body_Decl) = N_Subprogram_Body then
+ Spec_Id := Corresponding_Spec (Body_Decl);
+ else
+ Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
+ end if;
+
+ if No (Spec_Id) then
+ Error_Pragma ("pragma % cannot apply to a stand alone body");
+ return;
+ end if;
+
+ -- Refined_Pre/Post may only apply to the body [stub] of a subprogram
+ -- declared in the visible part of a package. Retrieve the context of
+ -- the subprogram declaration.
+
+ Spec_Decl := Parent (Parent (Spec_Id));
+
+ pragma Assert
+ (Nkind_In (Spec_Decl, N_Abstract_Subprogram_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration));
+
+ Pack_Spec := Parent (Spec_Decl);
+
+ if Nkind (Pack_Spec) /= N_Package_Specification
+ or else List_Containing (Spec_Decl) /=
+ Visible_Declarations (Pack_Spec)
+ then
+ Error_Pragma
+ ("pragma % must apply to the body of a visible subprogram");
+ return;
+ end if;
+
+ -- If we get here, the placement and legality of the pragma is OK
+
+ Legal := True;
+ end Analyze_Refined_Pre_Post;
+
--------------------------
-- Check_Ada_83_Warning --
--------------------------
@@ -15933,6 +16066,33 @@
when Pragma_Rational =>
Set_Rational_Profile;
+ ------------------
+ -- Refined_Post --
+ ------------------
+
+ -- pragma Refined_Post (boolean_EXPRESSION);
+
+ when Pragma_Refined_Post => Refined_Post : declare
+ Body_Decl : Node_Id;
+ Legal : Boolean;
+ Spec_Id : Entity_Id;
+
+ begin
+ -- Verify the legal placement of the pragma. The pragma is left
+ -- intentionally semi-analyzed. Process_PPCs does the remaining
+ -- analysis of the expression when Refined_Post is converted into
+ -- pragma Check.
+
+ Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal);
+
+ -- Analyze the expression when code generation is disabled because
+ -- the contract of the related subprogram will never be processed.
+
+ if Legal and then not Expander_Active then
+ Analyze_And_Resolve (Get_Pragma_Arg (Arg1), Standard_Boolean);
+ end if;
+ end Refined_Post;
+
-----------------
-- Refined_Pre --
-----------------
@@ -15940,139 +16100,46 @@
-- pragma Refined_Pre (boolean_EXPRESSION);
when Pragma_Refined_Pre => Refined_Pre : declare
- Body_Decl : Node_Id := Parent (N);
- Pack_Spec : Node_Id;
+ Body_Decl : Node_Id;
+ Legal : Boolean;
Restore : Boolean := False;
- Spec_Decl : Node_Id;
Spec_Id : Entity_Id;
- Stmt : Node_Id;
begin
- GNAT_Pragma;
- Check_Arg_Count (1);
- Check_No_Identifiers;
+ Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal);
- -- Verify the placement of the pragma and check for duplicates
+ if Legal then
+ pragma Assert (Present (Body_Decl));
+ pragma Assert (Present (Spec_Id));
- 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;
-
- -- The pragma applies to a subprogram body stub
-
- elsif Nkind (Stmt) = N_Subprogram_Body_Stub then
- Body_Decl := Stmt;
- exit;
-
- -- The pragma applies to an expression function that does not
- -- act as a completion of a previous function declaration.
-
- elsif Nkind (Stmt) = N_Subprogram_Declaration
- and then Nkind (Original_Node (Stmt)) = N_Expression_Function
- and then not
- Has_Completion (Defining_Unit_Name (Specification (Stmt)))
+ if Nkind (Body_Decl) = N_Subprogram_Body_Stub
+ and then No (Library_Unit (Body_Decl))
+ and then Current_Scope /= Spec_Id
then
- Error_Pragma ("pragma % cannot apply to a stand alone body");
- return;
-
- -- 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;
+ Restore := True;
+ Push_Scope (Spec_Id);
+ Install_Formals (Spec_Id);
end if;
- Stmt := Prev (Stmt);
- end loop;
+ -- Convert pragma Refined_Pre into pragma Check. The analysis
+ -- of the generated pragma will take care of the expression.
- -- Pragma Refined_Pre must apply to a subprogram body [stub]
+ Rewrite (N,
+ Make_Pragma (Loc,
+ Chars => Name_Check,
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_Identifier (Loc, Pname)),
- if not Nkind_In (Body_Decl, N_Subprogram_Body,
- N_Subprogram_Body_Stub)
- then
- Pragma_Misplaced;
- return;
- end if;
+ Make_Pragma_Argument_Association (Sloc (Arg1),
+ Expression => Relocate_Node (Get_Pragma_Arg (Arg1))))));
- -- The body [stub] must not act as a spec
+ Analyze (N);
- if Nkind (Body_Decl) = N_Subprogram_Body then
- Spec_Id := Corresponding_Spec (Body_Decl);
- else
- Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
+ if Restore then
+ Pop_Scope;
+ end if;
end if;
-
- if No (Spec_Id) then
- Error_Pragma ("pragma % cannot apply to a stand alone body");
- return;
- end if;
-
- -- Refined_Pre may only apply to the body [stub] of a subprogram
- -- declared in the visible part of a package. Retrieve the context
- -- of the subprogram declaration.
-
- Spec_Decl := Parent (Parent (Spec_Id));
-
- pragma Assert
- (Nkind_In (Spec_Decl, N_Abstract_Subprogram_Declaration,
- N_Generic_Subprogram_Declaration,
- N_Subprogram_Declaration));
-
- Pack_Spec := Parent (Spec_Decl);
-
- if Nkind (Pack_Spec) /= N_Package_Specification
- or else List_Containing (Spec_Decl) /=
- Visible_Declarations (Pack_Spec)
- then
- Error_Pragma
- ("pragma % must apply to the body of a visible subprogram");
- end if;
-
- -- When the pragma applies to a subprogram stub without a proper
- -- body, we have to restore the visibility of the stub and its
- -- formals to perform analysis.
-
- if Nkind (Body_Decl) = N_Subprogram_Body_Stub
- and then No (Library_Unit (Body_Decl))
- and then Current_Scope /= Spec_Id
- then
- Restore := True;
- Push_Scope (Spec_Id);
- Install_Formals (Spec_Id);
- end if;
-
- -- Convert pragma Refined_Pre into pragma Check. The analysis of
- -- the generated pragma will take care of the expression.
-
- Rewrite (N,
- Make_Pragma (Loc,
- Chars => Name_Check,
- Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Pname)),
-
- Make_Pragma_Argument_Association (Sloc (Arg1),
- Expression => Relocate_Node (Get_Pragma_Arg (Arg1))))));
-
- Analyze (N);
-
- if Restore then
- Pop_Scope;
- end if;
end Refined_Pre;
-----------------------
@@ -19158,6 +19225,7 @@
Pragma_Queuing_Policy => -1,
Pragma_Rational => -1,
Pragma_Ravenscar => -1,
+ Pragma_Refined_Post => -1,
Pragma_Refined_Pre => -1,
Pragma_Relative_Deadline => -1,
Pragma_Remote_Access_Type => -1,
@@ -19593,6 +19661,116 @@
end Process_Compilation_Unit_Pragmas;
+ ------------------------------
+ -- Relocate_Pragmas_To_Body --
+ ------------------------------
+
+ procedure Relocate_Pragmas_To_Body
+ (Subp_Body : Node_Id;
+ Target_Body : Node_Id := Empty)
+ is
+ procedure Relocate_Pragma (Prag : Node_Id);
+ -- Remove a single pragma from its current list and add it to the
+ -- declarations of the proper body (either Subp_Body or Target_Body).
+
+ ---------------------
+ -- Relocate_Pragma --
+ ---------------------
+
+ procedure Relocate_Pragma (Prag : Node_Id) is
+ Decls : List_Id;
+ Target : Node_Id;
+
+ begin
+ -- When subprogram stubs or expression functions are involves, the
+ -- destination declaration list belongs to the proper body.
+
+ if Present (Target_Body) then
+ Target := Target_Body;
+ else
+ Target := Subp_Body;
+ end if;
+
+ Decls := Declarations (Target);
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Declarations (Target, Decls);
+ end if;
+
+ -- Unhook the pragma from its current list
+
+ Remove (Prag);
+ Prepend (Prag, Decls);
+ end Relocate_Pragma;
+
+ -- Local variables
+
+ Body_Id : constant Entity_Id :=
+ Defining_Unit_Name (Specification (Subp_Body));
+ Next_Stmt : Node_Id;
+ Stmt : Node_Id;
+
+ -- Start of processing for Relocate_Pragmas_To_Body
+
+ begin
+ -- Do not process a body that comes from a separate unit as no construct
+ -- can possibly follow it.
+
+ if not Is_List_Member (Subp_Body) then
+ return;
+
+ -- Do not relocate pragmas that follow a stub if the stub does not have
+ -- a proper body.
+
+ elsif Nkind (Subp_Body) = N_Subprogram_Body_Stub
+ and then No (Target_Body)
+ then
+ return;
+
+ -- Do not process internally generated routine _Postconditions
+
+ elsif Ekind (Body_Id) = E_Procedure
+ and then Chars (Body_Id) = Name_uPostconditions
+ then
+ return;
+ end if;
+
+ -- Look at what is following the body. We are interested in certain kind
+ -- of pragmas (either from source or byproducts of expansion) that can
+ -- apply to a body [stub].
+
+ Stmt := Next (Subp_Body);
+ while Present (Stmt) loop
+
+ -- Preserve the following statement for iteration purposes due to a
+ -- possible relocation of a pragma.
+
+ Next_Stmt := Next (Stmt);
+
+ -- Move a candidate pragma following the body to the declarations of
+ -- the body.
+
+ if Nkind (Stmt) = N_Pragma
+ and then Pragma_On_Body_Or_Stub_OK (Get_Pragma_Id (Stmt))
+ then
+ Relocate_Pragma (Stmt);
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Stmt) then
+ null;
+
+ -- No candidate pragmas are available for relocation
+
+ else
+ exit;
+ end if;
+
+ Stmt := Next_Stmt;
+ end loop;
+ end Relocate_Pragmas_To_Body;
+
----------------------------
-- Rewrite_Assertion_Kind --
----------------------------
===================================================================
@@ -33,11 +33,15 @@
package Sem_Prag is
-- The following table lists all the implementation-defined pragmas that
- -- may apply to a body stub (no language defined pragmas apply).
+ -- may apply to a body stub (no language defined pragmas apply). The table
+ -- should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects if
+ -- the pragmas below implement an aspect.
- Pragma_On_Stub_OK : constant array (Pragma_Id) of Boolean :=
- (Pragma_Refined_Pre => True,
+ Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean :=
+ (Pragma_Refined_Post => True,
+ Pragma_Refined_Pre => True,
Pragma_SPARK_Mode => True,
+ Pragma_Warnings => True,
others => False);
-----------------
@@ -164,6 +168,15 @@
-- Suppress_All at this stage, since it can appear after the unit instead
-- of before (actually we allow it to appear anywhere).
+ procedure Relocate_Pragmas_To_Body
+ (Subp_Body : Node_Id;
+ Target_Body : Node_Id := Empty);
+ -- Resocate all pragmas that follow and apply to subprogram body Subp_Body
+ -- to its own declaration list. Candidate pragmas are classified in table
+ -- Pragma_On_Body_Or_Stub_OK. If Target_Body is set, the pragma are moved
+ -- to the declarations of Target_Body. This formal should be set when
+ -- dealing with subprogram body stubs or expression functions.
+
procedure Set_Encoded_Interface_Name (E : Entity_Id; S : Node_Id);
-- This routine is used to set an encoded interface name. The node S is an
-- N_String_Literal node for the external name to be set, and E is an
===================================================================
@@ -303,10 +303,6 @@
-- Verify that prefix of attribute N is a float type and that
-- two attribute expressions are present
- procedure Legal_Formal_Attribute;
- -- Common processing for attributes Definite and Has_Discriminants.
- -- Checks that prefix is generic indefinite formal type.
-
procedure Check_SPARK_Restriction_On_Attribute;
-- Issue an error in formal mode because attribute N is allowed
@@ -377,6 +373,14 @@
pragma No_Return (Error_Attr);
-- Like Error_Attr, but error is posted at the start of the prefix
+ function In_Refined_Post return Boolean;
+ -- Determine whether the current attribute appears in pragma
+ -- Refined_Post.
+
+ procedure Legal_Formal_Attribute;
+ -- Common processing for attributes Definite and Has_Discriminants.
+ -- Checks that prefix is generic indefinite formal type.
+
procedure Standard_Attribute (Val : Int);
-- Used to process attributes whose prefix is package Standard which
-- yield values of type Universal_Integer. The attribute reference
@@ -1927,6 +1931,60 @@
Error_Attr;
end Error_Attr_P;
+ ---------------------
+ -- In_Refined_Post --
+ ---------------------
+
+ function In_Refined_Post return Boolean is
+ function Is_Refined_Post (Prag : Node_Id) return Boolean;
+ -- Determine whether Prag denotes one of the incarnations of pragma
+ -- Refined_Post (either as is or pragma Check (Refined_Post, ...).
+
+ ---------------------
+ -- Is_Refined_Post --
+ ---------------------
+
+ function Is_Refined_Post (Prag : Node_Id) return Boolean is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+ Nam : constant Name_Id := Pragma_Name (Prag);
+
+ begin
+ if Nam = Name_Refined_Post then
+ return True;
+
+ elsif Nam = Name_Check then
+ pragma Assert (Present (Args));
+
+ return Chars (Expression (First (Args))) = Name_Refined_Post;
+ end if;
+
+ return False;
+ end Is_Refined_Post;
+
+ -- Local variables
+
+ Stmt : Node_Id;
+
+ -- Start of processing for In_Refined_Post
+
+ begin
+ Stmt := Parent (N);
+ while Present (Stmt) loop
+ if Nkind (Stmt) = N_Pragma and then Is_Refined_Post (Stmt) then
+ return True;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Stmt) then
+ exit;
+ end if;
+
+ Stmt := Parent (Stmt);
+ end loop;
+
+ return False;
+ end In_Refined_Post;
+
----------------------------
-- Legal_Formal_Attribute --
----------------------------
@@ -4281,7 +4339,32 @@
Error_Attr ("% attribute can only appear in postcondition", P);
end if;
- -- Body case, where we must be inside a generated _Postcondition
+ -- Check the legality of attribute 'Old when it appears inside pragma
+ -- Refined_Post. These specialized checks are required only when code
+ -- generation is disabled. In the general case pragma Refined_Post is
+ -- transformed into pragma Check by Process_PPCs which in turn is
+ -- relocated to procedure _Postconditions. From then on the legality
+ -- of 'Old is determined as usual.
+
+ elsif not Expander_Active and then In_Refined_Post then
+ Preanalyze_And_Resolve (P);
+ P_Type := Etype (P);
+ Set_Etype (N, P_Type);
+
+ if Is_Limited_Type (P_Type) then
+ Error_Attr ("attribute % cannot apply to limited objects", P);
+ end if;
+
+ if Is_Entity_Name (P)
+ and then Is_Constant_Object (Entity (P))
+ then
+ Error_Msg_N
+ ("??attribute Old applied to constant has no effect", P);
+ end if;
+
+ return;
+
+ -- Body case, where we must be inside a generated _Postconditions
-- procedure, or else the attribute use is definitely misplaced. The
-- postcondition itself may have generated transient scopes, and is
-- not necessarily the current one.
@@ -4302,8 +4385,8 @@
-- If the attribute reference is generated for a Requires clause,
-- then no expressions follow. Otherwise it is a primary, in which
- -- case, if expressions follow, the attribute reference must be
- -- an indexable object, so rewrite the node accordingly.
+ -- case, if expressions follow, the attribute reference must be an
+ -- indexable object, so rewrite the node accordingly.
if Present (E1) then
Rewrite (N,
@@ -4320,8 +4403,8 @@
Check_E0;
- -- Prefix has not been analyzed yet, and its full analysis will
- -- take place during expansion (see below).
+ -- Prefix has not been analyzed yet, and its full analysis will take
+ -- place during expansion (see below).
Preanalyze_And_Resolve (P);
P_Type := Etype (P);
@@ -4725,7 +4808,32 @@
Set_Is_Overloaded (P, False);
end if;
- -- Body case, where we must be inside a generated _Postcondition
+ -- Check the legality of attribute 'Result when it appears inside
+ -- pragma Refined_Post. These specialized checks are required only
+ -- when code generation is disabled. In the general case pragma
+ -- Refined_Post is transformed into pragma Check by Process_PPCs
+ -- which in turn is relocated to procedure _Postconditions. From
+ -- then on the legality of 'Result is determined as usual.
+
+ elsif not Expander_Active and then In_Refined_Post then
+ PS := Current_Scope;
+
+ -- The prefix denotes the proper related function
+
+ if Is_Entity_Name (P)
+ and then Ekind (Entity (P)) = E_Function
+ and then Entity (P) = PS
+ then
+ null;
+
+ else
+ Error_Msg_Name_2 := Chars (PS);
+ Error_Attr ("incorrect prefix for % attribute, expected %", P);
+ end if;
+
+ Set_Etype (N, Etype (PS));
+
+ -- Body case, where we must be inside a generated _Postconditions
-- procedure, and the prefix must be on the scope stack, or else the
-- attribute use is definitely misplaced. The postcondition itself
-- may have generated transient scopes, and is not necessarily the
@@ -4763,9 +4871,9 @@
null;
else
- Error_Msg_NE
- ("incorrect prefix for % attribute, expected &", P, PS);
- Error_Attr;
+ Error_Msg_Name_2 := Chars (PS);
+ Error_Attr
+ ("incorrect prefix for % attribute, expected %", P);
end if;
Rewrite (N, Make_Identifier (Sloc (N), Name_uResult));
===================================================================
@@ -466,6 +466,7 @@
Aspect_Pure_05 => Aspect_Pure_05,
Aspect_Pure_12 => Aspect_Pure_12,
Aspect_Pure_Function => Aspect_Pure_Function,
+ Aspect_Refined_Post => Aspect_Refined_Post,
Aspect_Refined_Pre => Aspect_Refined_Pre,
Aspect_Remote_Access_Type => Aspect_Remote_Access_Type,
Aspect_Remote_Call_Interface => Aspect_Remote_Call_Interface,
===================================================================
@@ -111,6 +111,7 @@
Aspect_Predicate, -- GNAT
Aspect_Priority,
Aspect_Read,
+ Aspect_Refined_Post, -- GNAT
Aspect_Refined_Pre, -- GNAT
Aspect_Relative_Deadline,
Aspect_Scalar_Storage_Order, -- GNAT
@@ -320,6 +321,7 @@
Aspect_Predicate => Expression,
Aspect_Priority => Expression,
Aspect_Read => Name,
+ Aspect_Refined_Post => Expression,
Aspect_Refined_Pre => Expression,
Aspect_Relative_Deadline => Expression,
Aspect_Scalar_Storage_Order => Expression,
@@ -417,6 +419,7 @@
Aspect_Pure_12 => Name_Pure_12,
Aspect_Pure_Function => Name_Pure_Function,
Aspect_Read => Name_Read,
+ Aspect_Refined_Post => Name_Refined_Post,
Aspect_Refined_Pre => Name_Refined_Pre,
Aspect_Relative_Deadline => Name_Relative_Deadline,
Aspect_Remote_Access_Type => Name_Remote_Access_Type,
@@ -639,6 +642,7 @@
Aspect_Convention => Never_Delay,
Aspect_Dimension => Never_Delay,
Aspect_Dimension_System => Never_Delay,
+ Aspect_Refined_Post => Never_Delay,
Aspect_Refined_Pre => Never_Delay,
Aspect_SPARK_Mode => Never_Delay,
Aspect_Synchronization => Never_Delay,
@@ -695,8 +699,12 @@
-- package P with SPARK_Mode ...;
-- package body P with SPARK_Mode is ...;
+ -- The table should be synchronized with Pragma_On_Body_Or_Stub_OK in unit
+ -- Sem_Prag if the aspects below are implemented by a pragma.
+
Aspect_On_Body_Or_Stub_OK : constant array (Aspect_Id) of Boolean :=
- (Aspect_Refined_Pre => True,
+ (Aspect_Refined_Post => True,
+ Aspect_Refined_Pre => True,
Aspect_SPARK_Mode => True,
Aspect_Warnings => True,
others => False);
===================================================================
@@ -349,15 +349,25 @@
Make_Handled_Sequence_Of_Statements (LocX,
Statements => New_List (Ret)));
+ -- If the expression completes a generic subprogram, we must create a
+ -- separate node for the body, because at instantiation the original
+ -- node of the generic copy must be a generic subprogram body, and
+ -- cannot be a expression function. Otherwise we just rewrite the
+ -- expression with the non-generic body.
+
if Present (Prev) and then Ekind (Prev) = E_Generic_Function then
+ Insert_After (N, New_Body);
- -- If the expression completes a generic subprogram, we must create a
- -- separate node for the body, because at instantiation the original
- -- node of the generic copy must be a generic subprogram body, and
- -- cannot be a expression function. Otherwise we just rewrite the
- -- expression with the non-generic body.
+ -- Propagate any aspects or pragmas that apply to the expression
+ -- function to the proper body when the expression function acts
+ -- as a completion.
- Insert_After (N, New_Body);
+ if Has_Aspects (N) then
+ Move_Aspects (N, To => New_Body);
+ end if;
+
+ Relocate_Pragmas_To_Body (New_Body);
+
Rewrite (N, Make_Null_Statement (Loc));
Set_Has_Completion (Prev, False);
Analyze (N);
@@ -371,6 +381,12 @@
Generate_Reference (Prev, Defining_Entity (N), 'b', Force => True);
Rewrite (N, New_Body);
+
+ -- Propagate any pragmas that apply to the expression function to the
+ -- proper body when the expression function acts as a completion.
+ -- Aspects are automatically transfered because of node rewriting.
+
+ Relocate_Pragmas_To_Body (N);
Analyze (N);
-- Prev is the previous entity with the same name, but it is can
@@ -11274,6 +11290,11 @@
-- under the same visibility conditions as for other invariant checks,
-- the type invariant must be applied to the returned value.
+ procedure Collect_Body_Postconditions (Post_Nam : Name_Id);
+ -- Examine the declarations of the body, looking for pragmas with name
+ -- Post_Nam. Parameter Post_Nam must denote either Name_Postcondition or
+ -- Name_Refined_Post. Chain any relevant postconditions to Plist.
+
function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id;
-- Prag contains an analyzed precondition or postcondition pragma. This
-- function copies the pragma, changes it to the corresponding Check
@@ -11365,6 +11386,60 @@
end if;
end Check_Access_Invariants;
+ ---------------------------------
+ -- Collect_Body_Postconditions --
+ ---------------------------------
+
+ procedure Collect_Body_Postconditions (Post_Nam : Name_Id) is
+ Next_Prag : Node_Id;
+
+ begin
+ pragma Assert
+ (Nam_In (Post_Nam, Name_Postcondition, Name_Refined_Post));
+
+ Prag := First (Declarations (N));
+ while Present (Prag) loop
+ Next_Prag := Next (Prag);
+
+ if Nkind (Prag) = N_Pragma then
+
+ -- Capture postcondition pragmas
+
+ if Pragma_Name (Prag) = Post_Nam then
+ Analyze (Prag);
+
+ -- All Refined_Post pragmas must be relocated to the body
+ -- of the generated _Postconditions routine, otherwise they
+ -- will be duplicated twice - once in the declarations of
+ -- the body and once in _Postconditions.
+
+ if Pragma_Name (Prag) = Name_Refined_Post then
+ Remove (Prag);
+ end if;
+
+ -- If expansion is disabled, as in a generic unit, save
+ -- pragma for later expansion.
+
+ if not Expander_Active then
+ Prepend (Grab_PPC, Declarations (N));
+ else
+ Append_Enabled_Item (Grab_PPC, Plist);
+ end if;
+ end if;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Prag) then
+ null;
+
+ else
+ exit;
+ end if;
+
+ Prag := Next_Prag;
+ end loop;
+ end Collect_Body_Postconditions;
+
--------------
-- Grab_PPC --
--------------
@@ -11791,6 +11866,8 @@
-- procedure _postconditions [(_Result : resulttype)] is
-- begin
+ -- pragma Check (Refined_Post, condition);
+ -- pragma Check (Refined_Post, condition);
-- pragma Check (Postcondition, condition [,message]);
-- pragma Check (Postcondition, condition [,message]);
-- ...
@@ -11801,44 +11878,9 @@
-- First we deal with the postconditions in the body
- if Is_Non_Empty_List (Declarations (N)) then
+ Collect_Body_Postconditions (Name_Refined_Post);
+ Collect_Body_Postconditions (Name_Postcondition);
- -- Loop through declarations
-
- Prag := First (Declarations (N));
- while Present (Prag) loop
- if Nkind (Prag) = N_Pragma then
-
- -- Capture postcondition pragmas
-
- if Pragma_Name (Prag) = Name_Postcondition then
- Analyze (Prag);
-
- -- If expansion is disabled, as in a generic unit, save
- -- pragma for later expansion.
-
- if not Expander_Active then
- Prepend (Grab_PPC, Declarations (N));
- else
- Append_Enabled_Item (Grab_PPC, Plist);
- end if;
- end if;
-
- Next (Prag);
-
- -- Not a pragma, if comes from source, then end scan
-
- elsif Comes_From_Source (Prag) then
- exit;
-
- -- Skip stuff not coming from source
-
- else
- Next (Prag);
- end if;
- end loop;
- end if;
-
-- Now deal with any postconditions from the spec
if Present (Spec_Id) then
===================================================================
@@ -1250,6 +1250,7 @@
Pragma_Pure_12 |
Pragma_Pure_Function |
Pragma_Queuing_Policy |
+ Pragma_Refined_Post |
Pragma_Refined_Pre |
Pragma_Relative_Deadline |
Pragma_Remote_Access_Type |
===================================================================
@@ -1928,6 +1928,15 @@
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_SPARK_Mode);
+ -- Refined_Post
+
+ when Aspect_Refined_Post =>
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Refined_Post);
+
-- Refined_Pre
when Aspect_Refined_Pre =>
@@ -7788,6 +7797,7 @@
Aspect_Postcondition |
Aspect_Pre |
Aspect_Precondition |
+ Aspect_Refined_Post |
Aspect_Refined_Pre |
Aspect_SPARK_Mode |
Aspect_Test_Case =>
===================================================================
@@ -580,6 +580,7 @@
Name_Pure_05 : constant Name_Id := N + $; -- GNAT
Name_Pure_12 : constant Name_Id := N + $; -- GNAT
Name_Pure_Function : constant Name_Id := N + $; -- GNAT
+ Name_Refined_Post : constant Name_Id := N + $; -- GNAT
Name_Refined_Pre : constant Name_Id := N + $; -- GNAT
Name_Relative_Deadline : constant Name_Id := N + $; -- Ada 05
Name_Remote_Access_Type : constant Name_Id := N + $; -- GNAT
@@ -1861,6 +1862,7 @@
Pragma_Pure_05,
Pragma_Pure_12,
Pragma_Pure_Function,
+ Pragma_Refined_Post,
Pragma_Refined_Pre,
Pragma_Relative_Deadline,
Pragma_Remote_Access_Type,
This patch provides the initial implementation of aspect/pragma Refined_Post. This construct is intended for formal verification proofs. The syntax of the aspect is as follows: ASPECT_DEFINITION ::= ( boolean_EXPRESSION ) The syntax of the pragma is as follows: pragma Refined_Post ( boolean_EXPRESSION ); The semantic rules of this construct are: A Refined_Post aspect may only appear on a body_stub (if one is present) or the body (if no stub is present) of a subprogram which is declared in the visible part of a package. The same legality rules apply to a Refined Postcondition as for a postcondition. A Refined Postcondition of a subprogram defines a refinement of the postcondition of the subprogram. Logically, the Refined Postcondition of a subprogram must imply its postcondition. This means that it is perfectly logical for the declaration not to have a postcondition (which in its absence defaults to True) but for the body or body stub to have a Refined Postcondition. For an expression_function without an explicit Refined Postcondition the expression implementing the function acts as its Refined Postcondition. The static semantics are otherwise as for a postcondition. When a subprogram with a Refined Postcondition is called; first the subprogram is evaluated. The Refined Postcondition is evaluated immediately before the evaluation of the postcondition or, if there is no postcondition, immediately before the point at which a postcondition would have been evaluated. If the Refined Postcondition evaluates to True then the postcondition is evaluated as described in the Ada RM. If either the Refined Postcondition or the postcondition do not evaluate to True then the exception Assertions.Assertion_Error is raised. ------------- -- Sources -- ------------- -- semantics.ads package Semantics is procedure OK_1 (Formal : out Integer) with Post => Formal > 12; procedure OK_2 (Formal : out Integer); procedure OK_3 (Formal : out Integer); procedure OK_4 (Formal : out Integer); function OK_5 (Formal : Integer) return Integer; procedure OK_6 (Formal : out Integer); procedure Error_1 (Formal : out Integer); procedure Error_2 (Formal : out Integer); procedure Error_3 (Formal : out Integer); function Error_9 (Formal : Integer) return Integer is -- not in body (Formal * Formal) with Refined_Post => Error_9'Result > 12; end Semantics; -- semantics.adb package body Semantics is Local : Integer; procedure OK_1 (Formal : out Integer) with Refined_Post => Formal + Local > 34 is begin null; end OK_1; procedure OK_2 (Formal : out Integer) with Refined_Post => Formal + Local > 34 is begin null; end OK_2; procedure OK_3 (Formal : out Integer) is separate with Refined_Post => Formal + Local > 34; procedure OK_4 (Formal : out Integer) is separate; pragma Refined_Post (Formal + Local > 34); package Nested_OK is procedure OK_4 (Formal : out Integer); end Nested_OK; package body Nested_OK is procedure OK_4 (Formal : out Integer) with Refined_Post => Formal + Local > 34 is begin null; end OK_4; end Nested_OK; function OK_5 (Formal : Integer) return Integer is (Formal * Local) with Refined_Post => OK_5'Result > 34; procedure OK_6 (Formal : out Integer) is separate; procedure Error_1 (Formal : out Integer) with Refined_Post => Local is -- expression must be boolean begin null; end Error_1; procedure Error_2 (Formal : out Integer) is separate -- expression must be with Refined_Post => Formal + 1; -- boolean, no body procedure Error_3 (Formal : out Integer) is separate; pragma Refined_Post (Formal + 1); -- expression must be boolean, no body procedure Error_4 (Formal : out Integer); procedure Error_4 (Formal : out Integer) with Refined_Post => Formal + Local > 654 is -- spec is not visible begin null; end Error_4; procedure Error_5 (Formal : out Integer) with Refined_Post => Formal > 321 is -- stand alone body begin null; end Error_5; package Nested_Error is private procedure Error_6 (Formal : out Integer); end Nested_Error; package body Nested_Error is procedure Error_6 (Formal : out Integer) with Refined_Post => Formal + Local > 34 is -- spec is not visible begin null; end Error_6; end Nested_Error; function Error_7 (Formal : Integer) return Integer is -- stand alone body (Formal * Local) with Refined_Post => Error_7'Result > 34; function Error_8 (Formal : Integer) return Integer; function Error_8 (Formal : Integer) return Integer is -- spec not visible (Formal * Local) with Refined_Post => Error_8'Result > 34; end Semantics; -- semantics-ok_3.adb separate (Semantics) procedure OK_3 (Formal : out Integer) is begin null; end OK_3; -- semantics-ok_4.adb separate (Semantics) procedure OK_4 (Formal : out Integer) is begin null; end OK_4; -- semantics-ok_6.adb separate (Semantics) procedure OK_6 (Formal : out Integer) with Refined_Post => (Formal + Local > 34) is begin null; end OK_6; -- dynamic_semantics.ads package Dynamic_Semantics is function Fail (Formal : Integer) return Integer with Post => Fail'Result > 20; -- Refined_Post => Fail'Result > 10 function Fail_Stub (Formal : Integer) return Integer with Post => Fail_Stub'Result > 20; -- Refined_Post => Fail_Stub'Result > 10 function Fail_Stub_2 (Formal : Integer) return Integer with Post => Fail_Stub_2'Result > 20; -- Refined_Post => Fail_Stub_2'Result > 10 procedure Set_Local (Val : Integer); end Dynamic_Semantics; -- dynamic_semantics.adb with Ada.Text_IO; use Ada.Text_IO; package body Dynamic_Semantics is Local : Integer := 0; function Fail (Formal : Integer) return Integer with Refined_Post => Fail'Result > 10 is begin return Formal + 1; end Fail; function Fail_Stub (Formal : Integer) return Integer is separate with Refined_Post => Fail_Stub'Result > 10; function Fail_Stub_2 (Formal : Integer) return Integer is separate; procedure Set_Local (Val : Integer) is begin Local := Val; end Set_Local; end Dynamic_Semantics; -- dynamic_semantics-fail_stub.adb separate (Dynamic_Semantics) function Fail_Stub (Formal : Integer) return Integer is begin return Formal + 1; end Fail_Stub; -- dynamic_semantics-fail_stub_2.adb separate (Dynamic_Semantics) function Fail_Stub_2 (Formal : Integer) return Integer with Refined_Post => Fail_Stub_2'Result > 10 is begin return Formal + 1; end Fail_Stub_2; -- main.adb with Ada.Assertions; use Ada.Assertions; with Ada.Exceptions; use Ada.Exceptions; with Ada.Text_IO; use Ada.Text_IO; with Dynamic_Semantics; use Dynamic_Semantics; procedure Main is Res : Integer; begin Set_Local (10); begin Res := Fail (5); Put_Line ("ERROR: Refined_Post did not fail (1)"); exception when E : Assertion_Error => Put_Line (Exception_Information (E)); when others => Put_Line ("ERROR: unexpected error (1)"); end; begin Res := Fail_Stub (5); Put_Line ("ERROR: Refined_Post on stub did not fail (2)"); exception when E : Assertion_Error => Put_Line (Exception_Information (E)); when others => Put_Line ("ERROR: unexpected error (2)"); end; begin Res := Fail_Stub_2 (5); Put_Line ("ERROR: Refined_Post on stub did not fail (3)"); exception when E : Assertion_Error => Put_Line (Exception_Information (E)); when others => Put_Line ("ERROR: unexpected error (3)"); end; Set_Local (30); begin Res := Fail (15); Put_Line ("ERROR: Post did not fail (4)"); exception when E : Assertion_Error => Put_Line (Exception_Information (E)); when others => Put_Line ("ERROR: unexpected error (4)"); end; begin Res := Fail_Stub (15); Put_Line ("ERROR: Post on stub did not fail (5)"); exception when E : Assertion_Error => Put_Line (Exception_Information (E)); when others => Put_Line ("ERROR: unexpected error (5)"); end; begin Res := Fail_Stub_2 (15); Put_Line ("ERROR: Post on stub did not fail (6)"); exception when E : Assertion_Error => Put_Line (Exception_Information (E)); when others => Put_Line ("ERROR: unexpected error (6)"); end; end Main; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnat12 -gnata semantics.adb $ gnatmake -q -gnat12 -gnata main.adb $ ./main semantics.adb:34:27: expected type "Standard.Boolean" semantics.adb:34:27: found type "Standard.Integer" semantics.adb:37:04: warning: subunit "Semantics.Error_2" in file "semantics-error_2.adb" not found semantics.adb:38:34: expected type "Standard.Boolean" semantics.adb:38:34: found type "Standard.Integer" semantics.adb:40:04: warning: subunit "Semantics.Error_3" in file "semantics-error_3.adb" not found semantics.adb:41:32: expected type "Standard.Boolean" semantics.adb:41:32: found type "Standard.Integer" semantics.adb:45:11: aspect "Refined_Post" must apply to the body of a visible subprogram semantics.adb:49:11: aspect "Refined_Post" cannot apply to a stand alone body semantics.adb:59:14: aspect "Refined_Post" must apply to the body of a visible subprogram semantics.adb:64:28: aspect "Refined_Post" cannot apply to a stand alone expression function semantics.adb:68:28: aspect "Refined_Post" must apply to the body of a visible subprogram semantics.ads:14:29: aspect "Refined_Post" cannot apply to a stand alone expression function Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE Message: Refined_Post failed at dynamic_semantics.adb:7 Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE Message: Refined_Post failed at dynamic_semantics.adb:13 Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE Message: Refined_Post failed at dynamic_semantics-fail_stub_2.adb:4 Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE Message: failed postcondition from dynamic_semantics.ads:3 Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE Message: failed postcondition from dynamic_semantics.ads:7 Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE Message: failed postcondition from dynamic_semantics.ads:11 Tested on x86_64-pc-linux-gnu, committed on trunk 2013-10-10 Hristian Kirtchev <kirtchev@adacore.com> * aspects.adb: Add an entry for Aspect_Refined_Post in table Canonical_Aspect. * aspects.ads: Add an entry for Aspect_Refined_Post in tables Aspect_Id, Aspect_Argument, Aspect_Names, Aspect_Delay, Aspect_On_Body_Or_Stub_OK. Update the comment on the use of table Aspect_On_Body_Or_Stub_OK. * par-prag.adb: Add pragma Refined_Post to the list of pragmas that do not require special processing by the parser. * sem_attr.adb (Analyze_Attribute): Add special analysis for attributes 'Old and 'Result when code generation is disabled and they appear in aspect/pragma Refined_Post. (In_Refined_Post): New routine. * sem_ch6.adb (Analyze_Expression_Function): Move various aspects and/or pragmas that apply to an expression function to the corresponding spec or body. (Collect_Body_Postconditions): New routine. (Process_PPCs): Use routine Collect_Body_Postconditions to gather all postcondition pragmas. * sem_ch10.adb (Analyze_Proper_Body): Use routine Relocate_Pragmas_To_Body to move all source pragmas that follow a body stub to the proper body. (Move_Stub_Pragmas_To_Body): Removed. * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing for aspect Refined_Post. (Check_Aspect_At_Freeze_Point): Aspect Refined_Post does not need delayed processing at the freeze point. * sem_prag.adb: Add an entry for pragma Refined_Post in table Sig_Flags. (Analyze_Pragma): Add processing for pragma Refined_Post. Update the processing of pragma Refined_Pre to use common routine Analyze_Refined_Pre_Post. (Analyze_Refined_Pre_Post): New routine. (Relocate_Pragmas_To_Body): New routine. * sem_prag.ads: Table Pragma_On_Stub_OK is now known as Pragma_On_Body_Or_Stub_OK. Update the comment on usage of table Pragma_On_Body_Or_Stub_OK. (Relocate_Pragmas_To_Body): New routine. * snames.ads-tmpl: Add new predefined name for Refined_Post. Add new Pragma_Id for Refined_Post.