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 <[email protected]>
* sem_attr.adb (Analyze_Attribute): add check during pre-analysis that
'Result only appears in postcondition of function.
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.
