Patchwork [Ada] Detect misplaced 'Result when compiling spec file

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 4, 2011, 9:43 a.m.
Message ID <20110804094323.GA11941@adacore.com>
Download mbox | patch
Permalink /patch/108394/
State New
Headers show

Comments

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
fixed.

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

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
+
       begin
          --  Find enclosing scopes, excluding loops
 
@@ -4029,6 +4032,23 @@ 
                Error_Attr;
             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.