This patch suppresses these false, which can occur when a postcondition
contains a quantified expression.
The following test should compile quietly.
gnatmake -f -gnat2012 -gnatwa t.adb
package T is
procedure P (S : in out String) with
Post => (for all C of S => C = C);
end T;
package body T is
procedure P (S : in out String) is
begin
null;
end P;
end T;
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-09-02 Bob Duff <[email protected]>
* sem_ch6.adb: (Check_Post_State): Suppress warning
"postcondition refers only to pre-state" when the expression has not
yet been analyzed, because it causes false alarms. This can happen when
the postcondition contains a quantified expression, because those are
analyzed later. This is a temporary/partial fix.
(Process_Post_Conditions): Minor: change wording of warning.
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 178459)
+++ sem_ch6.adb (working copy)
@@ -5551,9 +5551,16 @@
declare
E : constant Entity_Id := Entity (N);
begin
- if Is_Entity_Name (N)
- and then Present (E)
- and then Ekind (E) in Assignable_Kind
+ -- ???Quantified expressions get analyzed later, so E can be
+ -- empty at this point. In this case, we suppress the
+ -- warning, just in case E is assignable. It seems better to
+ -- have false negatives than false positives. At some point,
+ -- we should make the warning more accurate, either by
+ -- analyzing quantified expressions earlier, or moving this
+ -- processing later.
+
+ if No (E) or else
+ (Is_Entity_Name (N) and then Ekind (E) in Assignable_Kind)
then
Found := True;
end if;
@@ -5627,7 +5634,7 @@
Ignored := Find_Post_State (Arg);
if not Post_State_Mentioned then
- Error_Msg_N ("?postcondition only refers to pre-state",
+ Error_Msg_N ("?postcondition refers only to pre-state",
Prag);
end if;
end if;
