[Ada] Warning on suspicious existential quantifier
Arnaud Charlet
charlet@adacore.com
Thu Apr 25 10:49:00 GMT 2013
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_64pclinuxgnu, committed on trunk
20130425 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.
 next part 
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;

More information about the Gccpatches
mailing list