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 <kirtc...@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.
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;
-------------------
