[Ada] Detect misplaced 'Result when compiling spec file

Submitted by Arnaud Charlet on Aug. 4, 2011, 9:43 a.m.


Message ID 20110804094323.GA11941@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 4, 2011, 9:43 a.m.
A misplaced 'Result located in the precondition of a function was detected only
when compiling the body file, not when compiling the spec file. This is now

Compiling the following code raises an error:

$ gcc -c -gnat2012 -gnatc p.adb
p.ads:3:18: "Result" attribute can only appear in postcondition of function

package P is
   function F return Boolean
     with Pre => F'Result;
end P;

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

2011-08-04  Yannick Moy  <moy@adacore.com>

	* sem_attr.adb (Analyze_Attribute): add check during pre-analysis that
	'Result only appears in postcondition of function.

Patch hide | download patch | download mbox

Index: sem_attr.adb
--- sem_attr.adb	(revision 177343)
+++ sem_attr.adb	(working copy)
@@ -3990,6 +3990,9 @@ 
          --  source subprogram to which the postcondition applies. During
          --  pre-analysis, CS is the scope of the subprogram declaration.
+         Prag : Node_Id;
+         --  During pre-analysis, Prag is the enclosing pragma node if any
          --  Find enclosing scopes, excluding loops
@@ -4029,6 +4032,23 @@ 
             end if;
+            --  Check in postcondition of function
+            Prag := N;
+            while not Nkind_In (Prag, N_Pragma, N_Function_Specification,
+                                N_Subprogram_Body)
+            loop
+               Prag := Parent (Prag);
+            end loop;
+            if Nkind (Prag) /= N_Pragma
+              or else Get_Pragma_Id (Prag) /= Pragma_Postcondition
+            then
+               Error_Attr
+                 ("% attribute can only appear in postcondition of function",
+                  P);
+            end if;
             --  The attribute reference is a primary. If expressions follow,
             --  the attribute reference is really an indexable object, so
             --  rewrite and analyze as an indexed component.