Patchwork [Ada] Suppress false alarm "postcondition refers only to pre-state"

login
register
mail settings
Submitter Arnaud Charlet
Date Sept. 2, 2011, 10:05 a.m.
Message ID <20110902100504.GA2492@adacore.com>
Download mbox | patch
Permalink /patch/113093/
State New
Headers show

Comments

Arnaud Charlet - Sept. 2, 2011, 10:05 a.m.
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  <duff@adacore.com>

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

Patch

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;