[Ada] Order of evaluation between precondition and 'Old
Arnaud Charlet
charlet@adacore.com
Thu Feb 6 10:04:00 GMT 2014
This patch modifies the expansion of attribute 'Old to insert the generated
temporary that captures the value of the prefix before routine _Postconditions.
As a result, the precondition of a subprogram will be evaluated first, before
any postcondition-related code is executed.
------------
-- Source --
------------
-- evaluation_order.adb
procedure Evaluation_Order is
subtype Idx is Integer range 1 .. 10;
type Arr is array (Integer range <>) of Integer;
procedure Swap (A : in out Arr; X, Y : Idx)
with Pre => X in A'Range and Y in A'Range,
Post => A(X) = A(Y)'Old and A(Y) = A(X)'Old;
procedure Swap (A : in out Arr; X, Y : Idx) is begin null; end Swap;
A : Arr (1 .. 2) := (1 => 1, others => 0);
begin
Swap (A, 1, 3);
end Evaluation_Order;
----------------------------
-- Compilation and output --
----------------------------
$ gnatmake -q -gnata evaluation_order.adb
$ ./evaluation_order
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from
evaluation_order.adb:6
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-02-06 Hristian Kirtchev <kirtchev@adacore.com>
* exp_attr.adb (Expand_N_Attribute_Reference): Alphabetize
variables. Rename variabme Tnn to Temp. Do not create a temporary
if assertions are disabled. Find enclosing routine _Postconditions
and insert the temporary that captures the value of the prefix
before the routine.
* exp_ch6.adb (Build_Postconditions_Procedure):
Insert the generated _Postconditions routine
before the first source declaration of the related
subprogram.
(Insert_After_Last_Declaration): Removed.
(Insert_Before_First_Source_Declaration): New routine.
-------------- next part --------------
Index: exp_attr.adb
===================================================================
--- exp_attr.adb (revision 207533)
+++ exp_attr.adb (working copy)
@@ -3806,9 +3806,9 @@
---------
when Attribute_Old => Old : declare
- Tnn : constant Entity_Id := Make_Temporary (Loc, 'T', Pref);
+ Asn_Stm : Node_Id;
Subp : Node_Id;
- Asn_Stm : Node_Id;
+ Temp : Entity_Id;
begin
-- If assertions are disabled, no need to create the declaration
@@ -3818,42 +3818,47 @@
return;
end if;
- -- Find the nearest subprogram body, ignoring _Preconditions
+ Temp := Make_Temporary (Loc, 'T', Pref);
+ -- Climb the parent chain looking for subprogram _Postconditions
+
Subp := N;
- loop
+ while Present (Subp) loop
+ exit when Nkind (Subp) = N_Subprogram_Body
+ and then Chars (Defining_Entity (Subp)) = Name_uPostconditions;
+
Subp := Parent (Subp);
- exit when Nkind (Subp) = N_Subprogram_Body
- and then Chars (Defining_Entity (Subp)) /= Name_uPostconditions;
end loop;
- -- Insert the initialized object declaration at the start of the
- -- subprogram's declarations.
+ -- 'Old can only appear in a postcondition, the generated body of
+ -- _Postconditions must be in the tree.
+ pragma Assert (Present (Subp));
+
+ -- Generate:
+ -- Temp : constant <Pref type> := <Pref>;
+
Asn_Stm :=
Make_Object_Declaration (Loc,
- Defining_Identifier => Tnn,
+ Defining_Identifier => Temp,
Constant_Present => True,
Object_Definition => New_Occurrence_Of (Etype (N), Loc),
Expression => Pref);
- -- Push the subprogram's scope, so that the object will be analyzed
- -- in that context (rather than the context of the Precondition
- -- subprogram) and will have its Scope set properly.
+ -- Push the scope of the related subprogram where _Postcondition
+ -- resides as this ensures that the object will be analyzed in the
+ -- proper context.
- if Present (Corresponding_Spec (Subp)) then
- Push_Scope (Corresponding_Spec (Subp));
- else
- Push_Scope (Defining_Entity (Subp));
- end if;
+ Push_Scope (Scope (Defining_Entity (Subp)));
- if Is_Empty_List (Declarations (Subp)) then
- Set_Declarations (Subp, New_List (Asn_Stm));
- Analyze (Asn_Stm);
- else
- Insert_Action (First (Declarations (Subp)), Asn_Stm);
- end if;
+ -- The object declaration is inserted before the body of subprogram
+ -- _Postconditions. This ensures that any precondition-like actions
+ -- are still executed before any parameter values are captured and
+ -- the multiple 'Old occurrences appear in order of declaration.
+ Insert_Before_And_Analyze (Subp, Asn_Stm);
+ Pop_Scope;
+
-- Ensure that the prefix of attribute 'Old is valid. The check must
-- be inserted after the expansion of the attribute has taken place
-- to reflect the new placement of the prefix.
@@ -3862,9 +3867,7 @@
Ensure_Valid (Pref);
end if;
- Pop_Scope;
-
- Rewrite (N, New_Occurrence_Of (Tnn, Loc));
+ Rewrite (N, New_Occurrence_Of (Temp, Loc));
end Old;
----------------------
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb (revision 207536)
+++ exp_ch6.adb (working copy)
@@ -8911,27 +8911,47 @@
Stmts : List_Id;
Result : Entity_Id)
is
- procedure Insert_After_Last_Declaration (Stmt : Node_Id);
- -- Insert node Stmt after the last declaration of the subprogram body
+ procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id);
+ -- Insert node Stmt before the first source declaration of the
+ -- related subprogram's body. If no such declaration exists, Stmt
+ -- becomes the last declaration.
- -----------------------------------
- -- Insert_After_Last_Declaration --
- -----------------------------------
+ --------------------------------------------
+ -- Insert_Before_First_Source_Declaration --
+ --------------------------------------------
- procedure Insert_After_Last_Declaration (Stmt : Node_Id) is
- Decls : List_Id := Declarations (N);
+ procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is
+ Decls : constant List_Id := Declarations (N);
+ Decl : Node_Id;
begin
+ -- Inspect the declarations of the related subprogram body looking
+ -- for the first source declaration.
+
+ if Present (Decls) then
+ Decl := First (Decls);
+ while Present (Decl) loop
+ if Comes_From_Source (Decl) then
+ Insert_Before (Decl, Stmt);
+ return;
+ end if;
+
+ Next (Decl);
+ end loop;
+
+ -- If we get there, then the subprogram body lacks any source
+ -- declarations. The body of _Postconditions now acts as the
+ -- last declaration.
+
+ Append (Stmt, Decls);
+
-- Ensure that the body has a declaration list
- if No (Decls) then
- Decls := New_List;
- Set_Declarations (N, Decls);
+ else
+ Set_Declarations (N, New_List (Stmt));
end if;
+ end Insert_Before_First_Source_Declaration;
- Append_To (Decls, Stmt);
- end Insert_After_Last_Declaration;
-
-- Local variables
Loc : constant Source_Ptr := Sloc (N);
@@ -8965,9 +8985,9 @@
New_Reference_To (Etype (Result), Loc)));
end if;
- -- Insert _Postconditions after the last declaration of the body.
- -- This ensures that the body will not cause any premature freezing
- -- as it may mention types:
+ -- Insert _Postconditions before the first source declaration of the
+ -- body. This ensures that the body will not cause any premature
+ -- freezing as it may mention types:
-- procedure Proc (Obj : Array_Typ) is
-- procedure _postconditions is
@@ -8983,7 +9003,7 @@
-- order reference. The body of _Postconditions must be placed after
-- the declaration of Temp to preserve correct visibility.
- Insert_After_Last_Declaration (
+ Insert_Before_First_Source_Declaration (
Make_Subprogram_Body (Loc,
Specification =>
Make_Procedure_Specification (Loc,
More information about the Gcc-patches
mailing list