Patchwork [Ada] Warning for quantified expressions over null domains

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 2, 2012, 8:08 a.m.
Message ID <20121002080841.GA28960@adacore.com>
Download mbox | patch
Permalink /patch/188422/
State New
Headers show

Comments

Arnaud Charlet - Oct. 2, 2012, 8:08 a.m.
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  <schonberg@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.

Patch

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;