diff mbox

[Ada] Aspects Contract_Cases, Depends and Global not analyzed when applied to

Message ID 20130705103741.GA7717@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet July 5, 2013, 10:37 a.m. UTC 
This patch modifies the analysis of pragmas Contract_Cases, Depends and Global
to allow timely processing when the aspects or pragmas apply to a subprogram
compilation unit.

------------
-- Source --
------------

--  proc_aspects.ads

procedure Proc_Aspects (X : in out Integer) with
   Contract_Cases => (X => X + 1),
   Global         => Junk_Name_1,
   Depends        => ((Junk_Name_2, X) => (Junk_Name_3, X));

--  proc_pragmas.ads

procedure Proc_Pragmas (X : in out Integer);
pragma Contract_Cases ((X => X + 1));
pragma Global         (Junk_Name_1);
pragma Depends        (((Junk_Name_2, X) => (Junk_Name_3, X)));

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c -gnat12 -gnatd.V proc_aspects.ads
$ gcc -c -gnat12 -gnatd.V proc_pragmas.ads
proc_aspects.ads:2:23: expected type "Standard.Boolean"
proc_aspects.ads:2:23: found type "Standard.Integer"
proc_aspects.ads:2:30: expected type "Standard.Boolean"
proc_aspects.ads:2:30: found type "Standard.Integer"
proc_aspects.ads:3:22: "Junk_Name_1" is undefined
proc_aspects.ads:4:24: "Junk_Name_2" is undefined
proc_aspects.ads:4:44: "Junk_Name_3" is undefined
proc_pragmas.ads:2:25: expected type "Standard.Boolean"
proc_pragmas.ads:2:25: found type "Standard.Integer"
proc_pragmas.ads:2:32: expected type "Standard.Boolean"
proc_pragmas.ads:2:32: found type "Standard.Integer"
proc_pragmas.ads:3:24: "Junk_Name_1" is undefined
proc_pragmas.ads:4:26: "Junk_Name_2" is undefined
proc_pragmas.ads:4:46: "Junk_Name_3" is undefined

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

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

	* sem_prag.adb (Analyze_Pragma): Ensure that
	Contract_Cases, Depends and Global are analyzed when they apply
	to a subprogram compilation unit. The pragmas are all added
	unconditionally to the construct's contract. This ensures that
	proof tools can locate the pragmas.
diff mbox

Patch

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 200698)
+++ sem_prag.adb	(working copy)
@@ -10082,11 +10082,19 @@ 
             if Nkind (Subp_Decl) = N_Subprogram_Body then
                Analyze_Contract_Cases_In_Decl_Part (N);
 
+            --  When Contract_Cases applies to a subprogram compilation unit,
+            --  the corresponding pragma is placed after the unit's declaration
+            --  node and needs to be analyzed immediately.
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Declaration
+              and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit
+            then
+               Analyze_Contract_Cases_In_Decl_Part (N);
+            end if;
+
             --  Chain the pragma on the contract for further processing
 
-            else
-               Add_Contract_Item (N, Subp_Id);
-            end if;
+            Add_Contract_Item (N, Subp_Id);
          end Contract_Cases;
 
          ----------------
@@ -10590,11 +10598,19 @@ 
             if Nkind (Subp_Decl) = N_Subprogram_Body then
                Analyze_Depends_In_Decl_Part (N);
 
+            --  When Depends applies to a subprogram compilation unit, the
+            --  corresponding pragma is placed after the unit's declaration
+            --  node and needs to be analyzed immediately.
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Declaration
+              and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit
+            then
+               Analyze_Depends_In_Decl_Part (N);
+            end if;
+
             --  Chain the pragma on the contract for further processing
 
-            else
-               Add_Contract_Item (N, Subp_Id);
-            end if;
+            Add_Contract_Item (N, Subp_Id);
          end Depends;
 
          ---------------------
@@ -11833,11 +11849,19 @@ 
             if Nkind (Subp_Decl) = N_Subprogram_Body then
                Analyze_Global_In_Decl_Part (N);
 
+            --  When Global applies to a subprogram compilation unit, the
+            --  corresponding pragma is placed after the unit's declaration
+            --  node and needs to be analyzed immediately.
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Declaration
+              and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit
+            then
+               Analyze_Global_In_Decl_Part (N);
+            end if;
+
             --  Chain the pragma on the contract for further processing
 
-            else
-               Add_Contract_Item (N, Subp_Id);
-            end if;
+            Add_Contract_Item (N, Subp_Id);
          end Global;
 
          -----------
@@ -13348,8 +13372,8 @@ 
             --  abstract. ???
 
             if not Is_Tagged_Type (Typ) or else not Is_Abstract_Type (Typ) then
-               Error_Pragma_Arg ("pragma% requires an abstract "
-                 & "tagged type", Arg1);
+               Error_Pragma_Arg
+                 ("pragma% requires an abstract tagged type", Arg1);
 
             elsif not Has_Discriminants (Typ)
               or else Ekind (Etype (First_Discriminant (Typ)))