Patchwork [Ada] Wrong evaluation order for AND THEN in Pre/Post on library subprogram

login
register
mail settings
Submitter Arnaud Charlet
Date Jan. 2, 2013, 9:39 a.m.
Message ID <20130102093944.GA31935@adacore.com>
Download mbox | patch
Permalink /patch/208981/
State New
Headers show

Comments

Arnaud Charlet - Jan. 2, 2013, 9:39 a.m.
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  <quinot@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.

Patch

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));