diff mbox

[Ada] Interaction between packed arrays and post conditions

Message ID 20120402092108.GA16720@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet April 2, 2012, 9:21 a.m. UTC
This patch corrects the insertion of the compiler-generated routine which
encapsulates the behavior of post conditions. When a formal parameter is of a
packed array type, the compiler creates several helper subtypes and inserts
them at the top of the related subprogram declaration list. Since the post
conditions may reference formal parameters, the compiler-generated routine
_postconditions must be inserted after the last internal declaration at the
subprogram level.

Tested on x86_64-pc-linux-gnu, committed on trunk

2012-04-02  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch6.adb (Last_Implicit_Declaration): New routine.
	(Process_PPCs): Insert the body of _postconditions after the
	last internally generated declaration. This ensures that actual
	subtypes created for formal parameters are visible and properly
	frozen as _postconditions may reference them.
diff mbox

Patch

Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 186067)
+++ sem_ch6.adb	(working copy)
@@ -11057,6 +11057,9 @@ 
       --  that an invariant check is required (for an IN OUT parameter, or
       --  the returned value of a function.
 
+      function Last_Implicit_Declaration return Node_Id;
+      --  Return the last internally-generated declaration of N
+
       -------------
       -- Grab_CC --
       -------------
@@ -11307,6 +11310,50 @@ 
          end if;
       end Is_Public_Subprogram_For;
 
+      -------------------------------
+      -- Last_Implicit_Declaration --
+      -------------------------------
+
+      function Last_Implicit_Declaration return Node_Id is
+         Loc   : constant Source_Ptr := Sloc (N);
+         Decls : List_Id := Declarations (N);
+         Decl  : Node_Id;
+         Succ  : Node_Id;
+
+      begin
+         if No (Decls) then
+            Decls := New_List (Make_Null_Statement (Loc));
+            Set_Declarations (N, Decls);
+
+         elsif Is_Empty_List (Declarations (N)) then
+            Append_To (Decls, Make_Null_Statement (Loc));
+         end if;
+
+         --  Implicit and source declarations may be interspersed. Search for
+         --  the last implicit declaration which is either succeeded by a
+         --  source construct or is the last node in the declarative list.
+
+         Decl := First (Declarations (N));
+         while Present (Decl) loop
+            Succ := Next (Decl);
+
+            --  The current declaration is the last one, do not return Empty
+
+            if No (Succ) then
+               exit;
+
+            --  The successor is a source construct
+
+            elsif Comes_From_Source (Succ) then
+               exit;
+            end if;
+
+            Next (Decl);
+         end loop;
+
+         return Decl;
+      end Last_Implicit_Declaration;
+
    --  Start of processing for Process_PPCs
 
    begin
@@ -11712,7 +11759,7 @@ 
             --  The entity for the _Postconditions procedure
 
          begin
-            Prepend_To (Declarations (N),
+            Insert_After (Last_Implicit_Declaration,
               Make_Subprogram_Body (Loc,
                 Specification =>
                   Make_Procedure_Specification (Loc,