Patchwork [Ada] Consistency of aspect / pragma retrieval by compiler client tools

login
register
mail settings
Submitter Arnaud Charlet
Date July 8, 2013, 8:19 a.m.
Message ID <20130708081928.GA13458@adacore.com>
Download mbox | patch
Permalink /patch/257501/
State New
Headers show

Comments

Arnaud Charlet - July 8, 2013, 8:19 a.m.
This patch modifies the processing of pre- and postconditions that apply to
a body that acts as a spec to provide a uniform interface for compiler client
tools. The patch also augments routine Get_Pragma to retrieve delayed pragmas
stored in subprogram contracts.

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

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.

Patch

Index: einfo.adb
===================================================================
--- einfo.adb	(revision 200711)
+++ einfo.adb	(working copy)
@@ -6280,19 +6280,58 @@ 
    -- 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;
 
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 200753)
+++ einfo.ads	(working copy)
@@ -7375,7 +7375,9 @@ 
    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
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 200771)
+++ sem_prag.adb	(working copy)
@@ -3565,12 +3565,13 @@ 
          --  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 @@ 
                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;