Patchwork [Ada] Warning on suspicious existential quantifier

login
register
mail settings
Submitter Arnaud Charlet
Date April 25, 2013, 10:29 a.m.
Message ID <20130425102913.GA10737@adacore.com>
Download mbox | patch
Permalink /patch/239469/
State New
Headers show

Comments

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

--  semantics.ads

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>

	* sem_ch4.adb (Analyze_Quantified_Expression):
	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;
 
    -------------------