einfo.adb (Get_Pragma): Handle the retrieval of delayed pragmas stored in N_Contract nodes.

2013-07-08  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb (Get_Pragma): Handle the retrieval of delayed
	pragmas stored in N_Contract nodes.
	* einfo.ads (Get_Pragma): Update the comment on usage.
	* sem_prag.adb (Check_Precondition_Postcondition): Retain a copy
	of the pragma when it applies to a body that acts as a spec. The
	copy is preanalyzed and chained on the contract of the body.

From-SVN: r200774

4 files changed, 103 insertions, 18 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b508915..9178fc8 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,12 @@
+2013-07-08  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* einfo.adb (Get_Pragma): Handle the retrieval of delayed
+	pragmas stored in N_Contract nodes.
+	* einfo.ads (Get_Pragma): Update the comment on usage.
+	* sem_prag.adb (Check_Precondition_Postcondition): Retain a copy
+	of the pragma when it applies to a body that acts as a spec. The
+	copy is preanalyzed and chained on the contract of the body.
+
 2013-07-08  Robert Dewar  <dewar@adacore.com>
 
 	* rtsfind.adb: Minor comment fix.
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index bca2044..0ed0560 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -6280,19 +6280,58 @@ package body Einfo is
    -- Get_Pragma --
    ----------------
 
-   function Get_Pragma (E  : Entity_Id; Id : Pragma_Id) return Node_Id
-   is
-      N : Node_Id;
+   function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is
+      Is_CDG  : constant Boolean :=
+                  Id = Pragma_Depends or else Id = Pragma_Global;
+      Is_CTC  : constant Boolean :=
+                  Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case;
+      Is_PPC  : constant Boolean :=
+                  Id = Pragma_Precondition or else Id = Pragma_Postcondition;
+      Delayed : constant Boolean := Is_CDG or else Is_CTC or else Is_PPC;
+      Item    : Node_Id;
+      Items   : Node_Id;
 
    begin
-      N := First_Rep_Item (E);
-      while Present (N) loop
-         if Nkind (N) = N_Pragma
-           and then Get_Pragma_Id (Pragma_Name (N)) = Id
+      --  Handle delayed pragmas that appear in N_Contract nodes. Those have to
+      --  be extracted from their specialized list.
+
+      if Delayed then
+         Items := Contract (E);
+
+         if No (Items) then
+            return Empty;
+
+         elsif Is_CDG then
+            Item := Classifications (Items);
+
+         elsif Is_CTC then
+            Item := Contract_Test_Cases (Items);
+
+         else
+            Item := Pre_Post_Conditions (Items);
+         end if;
+
+      --  Regular pragmas
+
+      else
+         Item := First_Rep_Item (E);
+      end if;
+
+      while Present (Item) loop
+         if Nkind (Item) = N_Pragma
+           and then Get_Pragma_Id (Pragma_Name (Item)) = Id
          then
-            return N;
+            return Item;
+
+         --  All nodes in N_Contract are chained using Next_Pragma
+
+         elsif Delayed then
+            Item := Next_Pragma (Item);
+
+         --  Regular pragmas
+
          else
-            Next_Rep_Item (N);
+            Next_Rep_Item (Item);
          end if;
       end loop;
 
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index a998121..24bb12c 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -7375,7 +7375,9 @@ package Einfo is
    function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id;
    --  Searches the Rep_Item chain for a given entity E, for an instance of
    --  a pragma with the given pragma Id. If found, the value returned is the
-   --  N_Pragma node, otherwise Empty is returned.
+   --  N_Pragma node, otherwise Empty is returned. Delayed pragmas such as
+   --  Precondition, Postcondition, Contract_Cases, Depends and Global appear
+   --  in the N_Contract node of entity E and are also handled by this routine.
 
    function Get_Record_Representation_Clause (E : Entity_Id) return Node_Id;
    --  Searches the Rep_Item chain for a given entity E, for a record
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index a18b874..4fe6c57 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -3565,12 +3565,13 @@ package body Sem_Prag is
          --  If we fall through loop, pragma is at start of list, so see if it
          --  is at the start of declarations of a subprogram body.
 
-         if Nkind (Parent (N)) = N_Subprogram_Body
-           and then List_Containing (N) = Declarations (Parent (N))
+         PO := Parent (N);
+
+         if Nkind (PO) = N_Subprogram_Body
+           and then List_Containing (N) = Declarations (PO)
          then
-            if Operating_Mode /= Generate_Code
-              or else Inside_A_Generic
-            then
+            if Operating_Mode /= Generate_Code or else Inside_A_Generic then
+
                --  Analyze pragma expression for correctness and for ASIS use
 
                Preanalyze_Assert_Expression
@@ -3585,22 +3586,56 @@ package body Sem_Prag is
                end if;
             end if;
 
+            --  Retain a copy of the pre- or postcondition pragma for formal
+            --  verification purposes. The copy is needed because the pragma is
+            --  expanded into other constructs which are not acceptable in the
+            --  N_Contract node.
+
+            if Acts_As_Spec (PO)
+              and then (SPARK_Mode or else Formal_Extensions)
+            then
+               declare
+                  Prag : constant Node_Id := New_Copy_Tree (N);
+
+               begin
+                  --  Preanalyze the pragma
+
+                  Preanalyze_Assert_Expression
+                    (Get_Pragma_Arg
+                      (First (Pragma_Argument_Associations (Prag))),
+                     Standard_Boolean);
+
+                  --  Preanalyze the corresponding aspect (if any)
+
+                  if Present (Corresponding_Aspect (Prag)) then
+                     Preanalyze_Assert_Expression
+                       (Expression (Corresponding_Aspect (Prag)),
+                     Standard_Boolean);
+                  end if;
+
+                  --  Chain the copy on the contract of the body
+
+                  Add_Contract_Item
+                    (Prag, Defining_Unit_Name (Specification (PO)));
+               end;
+            end if;
+
             In_Body := True;
             return;
 
          --  See if it is in the pragmas after a library level subprogram
 
-         elsif Nkind (Parent (N)) = N_Compilation_Unit_Aux then
+         elsif Nkind (PO) = N_Compilation_Unit_Aux then
 
             --  In formal verification mode, analyze pragma expression for
             --  correctness, as it is not expanded later.
 
             if SPARK_Mode then
                Analyze_PPC_In_Decl_Part
-                 (N, Defining_Entity (Unit (Parent (Parent (N)))));
+                 (N, Defining_Entity (Unit (Parent (PO))));
             end if;
 
-            Chain_PPC (Unit (Parent (Parent (N))));
+            Chain_PPC (Unit (Parent (PO)));
             return;
          end if;