A universal quantified expression over a null domain is True. This result will
be counterintuitive for newcomers to Ada 2012, so it deserves an explicit
warning.
This patch also removes a spurious warning for such empty loops.
The commands:
gnatmake -q -gnat12 alfa
alfa
must yield:
alfa.adb:6:29:
warning: universal quantified expression over a null range has value True
alfa.adb:7:29:
warning: existential quantified expression over a null range has value False
TRUE
FALSE
---
with Ada.Text_IO; use Ada.Text_IO;
procedure Alfa is
type zzz is array (Integer range <>) of Integer;
B : zzz (2 .. 1) := (others => 0);
begin
Put_Line (Boolean'Image (for all E of B => E = 1));
Put_Line (Boolean'Image (for some E of B => E = 1));
end Alfa;
---
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-10-02 Ed Schonberg <schonb...@adacore.com>
* sem_ch4.adb (Analyze_Quantified_Expression): If the iterator in
a quantified expression is statically known to be null (e.g. a
array with an empty index type) emit a warning.
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb (revision 191900)
+++ sem_ch4.adb (working copy)
@@ -3404,6 +3404,38 @@
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.
+
+ function Is_Empty_Range (Typ : Entity_Id) return Boolean is
+ Loc : constant Source_Ptr := Sloc (N);
+
+ begin
+ if Is_Array_Type (Typ)
+ and then Size_Known_At_Compile_Time (Typ)
+ and then RM_Size (Typ) = 0
+ then
+ if All_Present (N) then
+ Error_Msg_N ("?universal quantified expression "
+ & "over a null range has value True", N);
+ Rewrite (N, New_Occurrence_Of (Standard_True, Loc));
+
+ else
+ Error_Msg_N ("?existential quantified expression "
+ & "over a null range has value False", N);
+ Rewrite (N, New_Occurrence_Of (Standard_False, Loc));
+ end if;
+
+ Analyze (N);
+ return True;
+
+ else
+ return False;
+ end if;
+ end Is_Empty_Range;
+
begin
Check_SPARK_Restriction ("quantified expression is not allowed", N);
@@ -3425,6 +3457,13 @@
if Present (Iterator_Specification (N)) then
Preanalyze (Iterator_Specification (N));
+
+ if Is_Entity_Name (Name (Iterator_Specification (N)))
+ and then Is_Empty_Range (Etype (Name (Iterator_Specification (N))))
+ then
+ return;
+ end if;
+
else
Preanalyze (Loop_Parameter_Specification (N));
end if;
