[Ada] Warning on suspicious existential quantifier

Message ID 20130425102913.GA10737@adacore.com New show

Commit Message

Arnaud Charlet April 25, 2013, 10:29 a.m.
```This patch adds a check in the analysis of quantified expressions to detect a
suspicious use of quantifier "some" when "all" was meant.

------------
-- Source --
------------

package Semantics is
function Error_1 (X : Integer) return Boolean
with
Post => (for some Y in Integer => (if Y > 5 then Error_1 (Y)));

function Error_2 (X : Integer) return Boolean
with
Post => (for some Y in Integer => (if Y > 5 then Error_2 (Y) else True));

function OK_1 (X : Integer) return Boolean
with
Post =>
(for some Y in Integer =>
(if Y > 5 then OK_1 (Y) else not OK_1 (Y)));

function OK_2 (X : Integer) return Boolean
with
Post =>
(for some Y in Integer =>
(if Y > 5 then OK_2 (Y) elsif Y = 5 then not OK_2 (Y)));

function Error_3 (X : Integer) return Boolean
with
Post =>
(for some X in Integer =>
(for some Y in Integer => (if X > 5 then Error_3 (Y))));

function OK_3 (X : Integer) return Boolean
with
Post => (for all Y in Integer => (if Y > 5 then OK_3 (Y)));

function OK_4 (X : Integer) return Boolean
with
Post => (for some Y in Integer => (OK_4 (Y)));

end Semantics;

----------------------------
-- Compilation and output --
----------------------------

\$ gcc -c -gnat12 -gnatd.V semantics.ads
semantics.ads:4:06: warning: function postcondition does not mention result
semantics.ads:4:15: warning: suspicious expression
semantics.ads:4:15: warning: did you mean (for all X => (if P then Q))
semantics.ads:4:15: warning: or (for some X => P and then Q) instead?
semantics.ads:8:06: warning: function postcondition does not mention result
semantics.ads:8:15: warning: suspicious expression
semantics.ads:8:15: warning: did you mean (for all X => (if P then Q))
semantics.ads:8:15: warning: or (for some X => P and then Q) instead?
semantics.ads:12:06: warning: function postcondition does not mention result
semantics.ads:18:06: warning: function postcondition does not mention result
semantics.ads:24:06: warning: function postcondition does not mention result
semantics.ads:26:11: warning: suspicious expression
semantics.ads:26:11: warning: did you mean (for all X => (if P then Q))
semantics.ads:26:11: warning: or (for some X => P and then Q) instead?
semantics.ads:30:06: warning: function postcondition does not mention result
semantics.ads:34:06: warning: function postcondition does not mention result

Tested on x86_64-pc-linux-gnu, committed on trunk

2013-04-25  Hristian Kirtchev  <kirtchev@adacore.com>

Warn on a suspicious use of quantifier "some" when "all" was meant.
(No_Else_Or_Trivial_True): New routine.
```

Patch

```Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb	(revision 198275)
+++ sem_ch4.adb	(working copy)
@@ -3501,13 +3501,15 @@
-----------------------------------

procedure Analyze_Quantified_Expression (N : Node_Id) is
-      QE_Scop : Entity_Id;
-
function Is_Empty_Range (Typ : Entity_Id) return Boolean;
--  If the iterator is part of a quantified expression, and the range is
--  known to be statically empty, emit a warning and replace expression
--  with its static value. Returns True if the replacement occurs.

+      function No_Else_Or_Trivial_True (If_Expr : Node_Id) return Boolean;
+      --  Determine whether if expression If_Expr lacks an else part or if it
+      --  has one, it evaluates to True.
+
--------------------
-- Is_Empty_Range --
--------------------
@@ -3545,6 +3547,25 @@
end if;
end Is_Empty_Range;

+      -----------------------------
+      -- No_Else_Or_Trivial_True --
+      -----------------------------
+
+      function No_Else_Or_Trivial_True (If_Expr : Node_Id) return Boolean is
+         Else_Expr : constant Node_Id :=
+                       Next (Next (First (Expressions (If_Expr))));
+      begin
+         return
+           No (Else_Expr)
+             or else (Compile_Time_Known_Value (Else_Expr)
+                       and then Is_True (Expr_Value (Else_Expr)));
+      end No_Else_Or_Trivial_True;
+
+      --  Local variables
+
+      Cond    : constant Node_Id := Condition (N);
+      QE_Scop : Entity_Id;
+
--  Start of processing for Analyze_Quantified_Expression

begin
@@ -3579,11 +3600,29 @@
Preanalyze (Loop_Parameter_Specification (N));
end if;

-      Preanalyze_And_Resolve (Condition (N), Standard_Boolean);
+      Preanalyze_And_Resolve (Cond, Standard_Boolean);

End_Scope;

Set_Etype (N, Standard_Boolean);
+
+      --  Diagnose a possible misuse of the "some" existential quantifier. When
+      --  we have a quantified expression of the form
+      --
+      --    for some X => (if P then Q [else True])
+      --
+      --  the if expression will not hold and render the quantified expression
+      --  trivially True.
+
+      if Formal_Extensions
+        and then not All_Present (N)
+        and then Nkind (Cond) = N_If_Expression
+        and then No_Else_Or_Trivial_True (Cond)
+      then
+         Error_Msg_N ("?suspicious expression", N);
+         Error_Msg_N ("\\did you mean (for all X ='> (if P then Q))", N);
+         Error_Msg_N ("\\or (for some X ='> P and then Q) instead'?", N);
+      end if;
end Analyze_Quantified_Expression;

-------------------

```