===================================================================
@@ -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.
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.