This change fixes the circuitry that processes Pre/Post aspects. Previously
when an AND THEN expression was used in such an aspect on a library level
subprogram, the operands would be evaluated in the wrong order.
Test case:
$ gnatmake -q call_p
$ ./call_p
F( 1) -> TRUE
F( 2) -> TRUE
P called
F( 1) -> TRUE
F( 2) -> FALSE
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed precondition from p.ads:2
-- gnat.adc
pragma Ada_2012;
pragma Check_Policy (Precondition, Check);
-- sources
with Ada.Exceptions;
with Ada.Text_IO; use Ada.Text_IO;
with Split_Pre_Order;
with P;
procedure Call_P is
begin
Split_Pre_Order.Pre_Array := (1 => True, 2 => True);
P;
Split_Pre_Order.Pre_Array (2) := False;
begin
P;
exception
when E : others =>
Put_Line (Ada.Exceptions.Exception_Information (E));
end;
end Call_P;
with Ada.Text_IO; use Ada.Text_IO;
procedure P is
begin
Put_Line ("P called");
end P;
with Split_Pre_Order;
procedure P with Pre => Split_Pre_Order.F (1) and then Split_Pre_Order.F (2);
pragma Ada_2012;
with Ada.Exceptions;
with Ada.Text_IO; use Ada.Text_IO;
pragma Check_Policy (Precondition, Check);
procedure Split_Pre_Order is
Pre_Array : array (1 .. 2) of Boolean;
function F (Index : Integer) return Boolean is
Result : constant Boolean := Pre_Array (Index);
begin
Put_Line ("F(" & Index'Img & ") -> " & Result'Img);
return Result;
end F;
procedure P with Pre => F (1) and then F (2);
procedure P is
begin
Put_Line ("P called");
end P;
begin
Pre_Array := (1 => True, 2 => True);
P;
Pre_Array := (1 => True, 2 => False);
begin
P;
exception
when E : others=>
Put_Line ("Exception raised: "
& Ada.Exceptions.Exception_Information (E));
end;
end Split_Pre_Order;
with Ada.Text_IO; use Ada.Text_IO;
package body Split_Pre_Order is
function F (Index : Integer) return Boolean is
Result : constant Boolean := Pre_Array (Index);
begin
Put_Line ("F(" & Index'Img & ") -> " & Result'Img);
return Result;
end F;
end Split_Pre_Order;
package Split_Pre_Order is
Pre_Array : array (1 .. 2) of Boolean;
function F (Index : Integer) return Boolean;
end Split_Pre_Order;
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-01-02 Thomas Quinot <qui...@adacore.com>
* sem_ch13.adb (Analyze_Aspect_Specifications): For a Pre/Post
aspect that applies to a library subprogram, prepend corresponding
pragma to the Pragmas_After list, in order for split AND THEN
sections to be processed in the expected order.
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 194782)
+++ sem_ch13.adb (working copy)
@@ -1602,11 +1602,22 @@
-- with delay of visibility for the expression analysis.
-- If the entity is a library-level subprogram, the pre/
- -- postconditions must be treated as late pragmas.
+ -- postconditions must be treated as late pragmas. Note
+ -- that they must be prepended, not appended, to the list,
+ -- so that split AND THEN sections are processed in the
+ -- correct order.
if Nkind (Parent (N)) = N_Compilation_Unit then
- Add_Global_Declaration (Aitem);
+ declare
+ Aux : constant Node_Id := Aux_Decls_Node (Parent (N));
+ begin
+ if No (Pragmas_After (Aux)) then
+ Set_Pragmas_After (Aux, New_List);
+ end if;
+ Prepend (Aitem, Pragmas_After (Aux));
+ end;
+
-- If it is a subprogram body, add pragmas to list of
-- declarations in body.
@@ -1930,7 +1941,7 @@
else
if No (Pragmas_After (Aux)) then
- Set_Pragmas_After (Aux, Empty_List);
+ Set_Pragmas_After (Aux, New_List);
end if;
Append (Aitem, Pragmas_After (Aux));
