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 <kirtc...@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.
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)))
