Patchwork [Ada] Spurious error in case expression of static predicate subtype

login
register
mail settings
Submitter Arnaud Charlet
Date April 11, 2013, 1:10 p.m.
Message ID <20130411131042.GA18179@adacore.com>
Download mbox | patch
Permalink /patch/235736/
State New
Headers show

Comments

Arnaud Charlet - April 11, 2013, 1:10 p.m.
This patch corrects the implementation of static predicates in the context of
case expressions and/or statements. The maching of individual case alternatives
is now done against the sets of legal values defined by the static predicate.

------------
-- Source --
------------

--  static_predicates.adb

procedure Static_Predicates is
   type Typ is (A, B, C, D, E, F, G, H, I, J, K, L, M, N);

   subtype Subtyp is Typ with
     Static_Predicate => Subtyp in D .. F | H | J .. L;

   --  0  1  2  3  4  5  6  7  8  9  10 11 12 13
   --          +-------+   +-+   +-------+
   --  A  B  C |D  E  F| G |H| I |J  K  L| M  N
   --          +-------+   +-+   +-------+

   Obj : Subtyp;

begin
   case Obj is
      when A .. B => null;  --  A .. B  illegal
   end case;
   case Obj is
      when B .. D => null;  --  B .. C  illegal
   end case;
   case Obj is              --  missing F, H, J .. L
      when D .. E => null;
   end case;
   case Obj is
      when E .. G => null;  --  G  illegal
   end case;
   case Obj is
      when F .. H => null;  --  G  illegal
   end case;
   case Obj is              --  missing D .. F
      when G .. H => null;  --  G  illegal
   end case;
   case Obj is              --  missing D .. F
      when H .. I => null;  --  I  illegal
   end case;
   case Obj is              --  missing D .. F, H
      when I .. M => null;  --  I illegal
   end case;
   case Obj is              --  ok
      when D .. F => null;
      when H      => null;
      when J .. L => null;
   end case;
   case Obj is
      when D .. E => null;
      when G .. N => null;  --  G  illegal
      when others => null;
   end case;
   case Obj is
      when D      => null;
      when D .. F => null;  --  D  duplicated
      when H      => null;
      when J .. L => null;
   end case;
   case Obj is
      when D .. F => null;
      when H      => null;
      when J .. L => null;
      when J      => null;  --  J  duplicated
   end case;
end Static_Predicates;

----------------------------
-- Compilation and output --
----------------------------

gcc -c -gnat12 static_predicates.adb
static_predicates.adb:16:14: static predicate on "Subtyp" excludes range
  "A" .. "B"
static_predicates.adb:19:14: static predicate on "Subtyp" excludes range
  "B" .. "C"
static_predicates.adb:21:04: missing case value: "F"
static_predicates.adb:21:04: missing case value: "H"
static_predicates.adb:21:04: missing case values: "J" .. "L"
static_predicates.adb:25:14: static predicate on "Subtyp" excludes value "G"
static_predicates.adb:28:14: static predicate on "Subtyp" excludes value "G"
static_predicates.adb:30:04: missing case values: "D" .. "F"
static_predicates.adb:31:14: static predicate on "Subtyp" excludes value "G"
static_predicates.adb:33:04: missing case values: "D" .. "F"
static_predicates.adb:34:14: static predicate on "Subtyp" excludes value "I"
static_predicates.adb:36:04: missing case values: "D" .. "F"
static_predicates.adb:36:04: missing case value: "H"
static_predicates.adb:37:14: static predicate on "Subtyp" excludes value "I"
static_predicates.adb:46:14: static predicate on "Subtyp" excludes value "G"
static_predicates.adb:50:12: duplication of choice value
static_predicates.adb:58:14: duplication of choice value

Tested on x86_64-pc-linux-gnu, committed on trunk

2013-04-11  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_case.adb (Check_Against_Predicate): New routine.
	(Check_Choices): When the type covered by the list of choices
	is a static subtype with a static predicate, check all choices
	agains the predicate.
	(Issue_Msg): All versions removed.
	(Missing_Choice): New routines.
	* sem_ch4.adb: Code and comment reformatting.
	(Analyze_Case_Expression): Do not check the choices when the case
	expression is being preanalyzed and the type of the expression
	is a subtype with a static predicate.
	(Has_Static_Predicate): New routine.
	* sem_ch13.adb: Code and comment reformatting.	(Build_Range):
	Always build a range even if the low and hi bounds denote the
	same value. This is needed by the machinery in Check_Choices.
	(Build_Static_Predicate): Always build a range even if the low and
	hi bounds denote the same value. This is needed by the machinery
	in Check_Choices.

Patch

Index: sem_case.adb
===================================================================
--- sem_case.adb	(revision 197743)
+++ sem_case.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1996-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1996-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -114,6 +114,18 @@ 
       Others_Present : Boolean;
       Case_Node      : Node_Id)
    is
+      procedure Check_Against_Predicate
+        (Pred    : in out Node_Id;
+         Choice  : Choice_Bounds;
+         Prev_Lo : in out Uint;
+         Prev_Hi : in out Uint;
+         Error   : in out Boolean);
+      --  Determine whether a choice covers legal values as defined by a static
+      --  predicate set. Pred is a static predicate range. Choice is the choice
+      --  to be examined. Prev_Lo and Prev_Hi are the bounds of the previous
+      --  choice that covered a predicate set. Error denotes whether the check
+      --  found an illegal intersection.
+
       procedure Explain_Non_Static_Bound;
       --  Called when we find a non-static bound, requiring the base type to
       --  be covered. Provides where possible a helpful explanation of why the
@@ -123,103 +135,293 @@ 
       --  Comparison routine for comparing Choice_Table entries. Use the lower
       --  bound of each Choice as the key.
 
+      procedure Missing_Choice (Value1 : Node_Id; Value2 : Node_Id);
+      procedure Missing_Choice (Value1 : Node_Id; Value2 : Uint);
+      procedure Missing_Choice (Value1 : Uint;    Value2 : Node_Id);
+      procedure Missing_Choice (Value1 : Uint;    Value2 : Uint);
+      --  Issue an error message indicating that there are missing choices,
+      --  followed by the image of the missing choices themselves which lie
+      --  between Value1 and Value2 inclusive.
+
+      procedure Missing_Choices (Pred : Node_Id; Prev_Hi : Uint);
+      --  Emit an error message for each non-covered static predicate set.
+      --  Prev_Hi denotes the upper bound of the last choice that covered a
+      --  set.
+
       procedure Move_Choice (From : Natural; To : Natural);
       --  Move routine for sorting the Choice_Table
 
       package Sorting is new GNAT.Heap_Sort_G (Move_Choice, Lt_Choice);
 
-      procedure Issue_Msg (Value1 : Node_Id; Value2 : Node_Id);
-      procedure Issue_Msg (Value1 : Node_Id; Value2 : Uint);
-      procedure Issue_Msg (Value1 : Uint;    Value2 : Node_Id);
-      procedure Issue_Msg (Value1 : Uint;    Value2 : Uint);
-      --  Issue an error message indicating that there are missing choices,
-      --  followed by the image of the missing choices themselves which lie
-      --  between Value1 and Value2 inclusive.
+      -----------------------------
+      -- Check_Against_Predicate --
+      -----------------------------
 
-      ---------------
-      -- Issue_Msg --
-      ---------------
+      procedure Check_Against_Predicate
+        (Pred    : in out Node_Id;
+         Choice  : Choice_Bounds;
+         Prev_Lo : in out Uint;
+         Prev_Hi : in out Uint;
+         Error   : in out Boolean)
+      is
+         procedure Illegal_Range
+           (Loc : Source_Ptr;
+            Lo  : Uint;
+            Hi  : Uint);
+         --  Emit an error message regarding a choice that clashes with the
+         --  legal static predicate sets. Loc is the location of the choice
+         --  that introduced the illegal range. Lo .. Hi is the range.
 
-      procedure Issue_Msg (Value1 : Node_Id; Value2 : Node_Id) is
-      begin
-         Issue_Msg (Expr_Value (Value1), Expr_Value (Value2));
-      end Issue_Msg;
+         function Inside_Range
+           (Lo  : Uint;
+            Hi  : Uint;
+            Val : Uint) return Boolean;
+         --  Determine whether position Val within a discrete type is within
+         --  the range Lo .. Hi inclusive.
 
-      procedure Issue_Msg (Value1 : Node_Id; Value2 : Uint) is
-      begin
-         Issue_Msg (Expr_Value (Value1), Value2);
-      end Issue_Msg;
+         -------------------
+         -- Illegal_Range --
+         -------------------
 
-      procedure Issue_Msg (Value1 : Uint; Value2 : Node_Id) is
-      begin
-         Issue_Msg (Value1, Expr_Value (Value2));
-      end Issue_Msg;
+         procedure Illegal_Range
+           (Loc : Source_Ptr;
+            Lo  : Uint;
+            Hi  : Uint)
+         is
+         begin
+            Error_Msg_Name_1 := Chars (Bounds_Type);
 
-      procedure Issue_Msg (Value1 : Uint; Value2 : Uint) is
-         Msg_Sloc : constant Source_Ptr := Sloc (Case_Node);
+            --  Single value
 
+            if Lo = Hi then
+               if Is_Integer_Type (Bounds_Type) then
+                  Error_Msg_Uint_1 := Lo;
+                  Error_Msg ("static predicate on % excludes value ^!", Loc);
+               else
+                  Error_Msg_Name_2 := Choice_Image (Lo, Bounds_Type);
+                  Error_Msg ("static predicate on % excludes value %!", Loc);
+               end if;
+
+            --  Range
+
+            else
+               if Is_Integer_Type (Bounds_Type) then
+                  Error_Msg_Uint_1 := Lo;
+                  Error_Msg_Uint_2 := Hi;
+                  Error_Msg
+                    ("static predicate on % excludes range ^ .. ^!", Loc);
+               else
+                  Error_Msg_Name_2 := Choice_Image (Lo, Bounds_Type);
+                  Error_Msg_Name_3 := Choice_Image (Hi, Bounds_Type);
+                  Error_Msg
+                    ("static predicate on % excludes range % .. %!", Loc);
+               end if;
+            end if;
+         end Illegal_Range;
+
+         ------------------
+         -- Inside_Range --
+         ------------------
+
+         function Inside_Range
+           (Lo  : Uint;
+            Hi  : Uint;
+            Val : Uint) return Boolean
+         is
+         begin
+            return
+              Val = Lo or else Val = Hi or else (Lo < Val and then Val < Hi);
+         end Inside_Range;
+
+         --  Local variables
+
+         Choice_Hi : constant Uint := Expr_Value (Choice.Hi);
+         Choice_Lo : constant Uint := Expr_Value (Choice.Lo);
+         Loc       : Source_Ptr;
+         Next_Hi   : Uint;
+         Next_Lo   : Uint;
+         Pred_Hi   : Uint;
+         Pred_Lo   : Uint;
+
+      --  Start of processing for Check_Against_Predicate
+
       begin
-         --  AI05-0188 : within an instance the non-others choices do not
-         --  have to belong to the actual subtype.
+         --  Find the proper error message location
 
-         if Ada_Version >= Ada_2012 and then In_Instance then
-            return;
+         if Present (Choice.Node) then
+            Loc := Sloc (Choice.Node);
+         else
+            Loc := Sloc (Case_Node);
          end if;
 
-         --  In some situations, we call this with a null range, and
-         --  obviously we don't want to complain in this case!
+         if Present (Pred) then
+            Pred_Lo := Expr_Value (Low_Bound  (Pred));
+            Pred_Hi := Expr_Value (High_Bound (Pred));
 
-         if Value1 > Value2 then
+         --  Previous choices managed to satisfy all static predicate sets
+
+         else
+            Illegal_Range (Loc, Choice_Lo, Choice_Hi);
+            Error := True;
+
             return;
          end if;
 
-         --  Case of only one value that is missing
+         --  Step 1: Detect duplicate choices
 
-         if Value1 = Value2 then
-            if Is_Integer_Type (Bounds_Type) then
-               Error_Msg_Uint_1 := Value1;
-               Error_Msg ("missing case value: ^!", Msg_Sloc);
+         if Inside_Range (Choice_Lo, Choice_Hi, Prev_Lo)
+           or else Inside_Range (Choice_Lo, Choice_Hi, Prev_Hi)
+         then
+            Error_Msg ("duplication of choice value", Loc);
+            Error := True;
+
+         --  Step 2: Detect full coverage
+
+         --  Choice_Lo    Choice_Hi
+         --  +============+
+         --  Pred_Lo      Pred_Hi
+
+         elsif Choice_Lo = Pred_Lo and then Choice_Hi = Pred_Hi then
+            Prev_Lo := Choice_Lo;
+            Prev_Hi := Choice_Hi;
+            Next (Pred);
+
+         --  Step 3: Detect all cases where a choice mentions values that are
+         --  not part of the static predicate sets.
+
+         --  Choice_Lo   Choice_Hi   Pred_Lo   Pred_Hi
+         --  +-----------+ . . . . . +=========+
+         --   ^ illegal ^
+
+         elsif Choice_Lo < Pred_Lo and then Choice_Hi < Pred_Lo then
+            Illegal_Range (Loc, Choice_Lo, Choice_Hi);
+            Error := True;
+
+         --  Choice_Lo   Pred_Lo   Choice_Hi   Pred_Hi
+         --  +-----------+=========+===========+
+         --   ^ illegal ^
+
+         elsif Choice_Lo < Pred_Lo
+           and then Inside_Range (Pred_Lo, Pred_Hi, Choice_Hi)
+         then
+            Illegal_Range (Loc, Choice_Lo, Pred_Lo - 1);
+            Error := True;
+
+         --  Pred_Lo   Pred_Hi   Choice_Lo   Choice_Hi
+         --  +=========+ . . . . +-----------+
+         --                       ^ illegal ^
+
+         elsif Pred_Lo < Choice_Lo and then Pred_Hi < Choice_Lo then
+            Missing_Choice (Pred_Lo, Pred_Hi);
+            Error := True;
+
+            --  There may be several static predicate sets between the current
+            --  one and the choice. Inspect the next static predicate set.
+
+            Next (Pred);
+            Check_Against_Predicate
+              (Pred    => Pred,
+               Choice  => Choice,
+               Prev_Lo => Prev_Lo,
+               Prev_Hi => Prev_Hi,
+               Error   => Error);
+
+         --  Pred_Lo   Choice_Lo   Pred_Hi     Choice_Hi
+         --  +=========+===========+-----------+
+         --                         ^ illegal ^
+
+         elsif Pred_Hi < Choice_Hi
+           and then Inside_Range (Pred_Lo, Pred_Hi, Choice_Lo)
+         then
+            Next (Pred);
+
+            --  The choice may fall in a static predicate set. If this is the
+            --  case, avoid mentioning legal values in the error message.
+
+            if Present (Pred) then
+               Next_Lo := Expr_Value (Low_Bound  (Pred));
+               Next_Hi := Expr_Value (High_Bound (Pred));
+
+               --  The next static predicate set is to the right of the choice
+
+               if Choice_Hi < Next_Lo and then Choice_Hi < Next_Hi then
+                  Illegal_Range (Loc, Pred_Hi + 1, Choice_Hi);
+               else
+                  Illegal_Range (Loc, Pred_Hi + 1, Next_Lo - 1);
+               end if;
             else
-               Error_Msg_Name_1 := Choice_Image (Value1, Bounds_Type);
-               Error_Msg ("missing case value: %!", Msg_Sloc);
+               Illegal_Range (Loc, Pred_Hi + 1, Choice_Hi);
             end if;
 
-         --  More than one choice value, so print range of values
+            Error := True;
 
+         --  Choice_Lo   Pred_Lo   Pred_Hi     Choice_Hi
+         --  +-----------+=========+-----------+
+         --   ^ illegal ^           ^ illegal ^
+
+         --  Emit an error on the low gap, disregard the upper gap
+
+         elsif Choice_Lo < Pred_Lo and then Pred_Hi < Choice_Hi then
+            Illegal_Range (Loc, Choice_Lo, Pred_Lo - 1);
+            Error := True;
+
+         --  Step 4: Detect all cases of partial or missing coverage
+
+         --  Pred_Lo   Choice_Lo  Choice_Hi   Pred_Hi
+         --  +=========+==========+===========+
+         --   ^  gap  ^            ^   gap   ^
+
          else
-            if Is_Integer_Type (Bounds_Type) then
-               Error_Msg_Uint_1 := Value1;
-               Error_Msg_Uint_2 := Value2;
-               Error_Msg ("missing case values: ^ .. ^!", Msg_Sloc);
-            else
-               Error_Msg_Name_1 := Choice_Image (Value1, Bounds_Type);
-               Error_Msg_Name_2 := Choice_Image (Value2, Bounds_Type);
-               Error_Msg ("missing case values: % .. %!", Msg_Sloc);
-            end if;
-         end if;
-      end Issue_Msg;
+            --  An "others" choice covers all gaps
 
-      ---------------
-      -- Lt_Choice --
-      ---------------
+            if Others_Present then
+               Prev_Lo := Choice_Lo;
+               Prev_Hi := Choice_Hi;
+               Next (Pred);
 
-      function Lt_Choice (C1, C2 : Natural) return Boolean is
-      begin
-         return
-           Expr_Value (Choice_Table (Nat (C1)).Lo)
-             <
-           Expr_Value (Choice_Table (Nat (C2)).Lo);
-      end Lt_Choice;
+            --  Choice_Lo   Choice_Hi   Pred_Hi
+            --  +===========+===========+
+            --  Pred_Lo      ^   gap   ^
 
-      -----------------
-      -- Move_Choice --
-      -----------------
+            --  The upper gap may be covered by a subsequent choice
 
-      procedure Move_Choice (From : Natural; To : Natural) is
-      begin
-         Choice_Table (Nat (To)) := Choice_Table (Nat (From));
-      end Move_Choice;
+            elsif Pred_Lo = Choice_Lo then
+               Prev_Lo := Choice_Lo;
+               Prev_Hi := Choice_Hi;
 
+            --  Pred_Lo     Prev_Hi   Choice_Lo   Choice_Hi   Pred_Hi
+            --  +===========+=========+===========+===========+
+            --   ^ covered ^ ^  gap  ^
+
+            else pragma Assert (Pred_Lo < Choice_Lo);
+
+               --  A previous choice covered the gap up to the current choice
+
+               if Prev_Hi = Choice_Lo - 1 then
+                  Prev_Lo := Choice_Lo;
+                  Prev_Hi := Choice_Hi;
+
+                  if Choice_Hi = Pred_Hi then
+                     Next (Pred);
+                  end if;
+
+               --  The previous choice did not intersect with the current
+               --  static predicate set.
+
+               elsif Prev_Hi < Pred_Lo then
+                  Missing_Choice (Pred_Lo, Choice_Lo - 1);
+                  Error := True;
+
+               --  The previous choice covered part of the static predicate set
+
+               else
+                  Missing_Choice (Prev_Hi, Choice_Lo - 1);
+                  Error := True;
+               end if;
+            end if;
+         end if;
+      end Check_Against_Predicate;
+
       ------------------------------
       -- Explain_Non_Static_Bound --
       ------------------------------
@@ -236,16 +438,16 @@ 
 
          if Bounds_Type /= Subtyp then
 
-            --  If the case is a variant part, the expression is given by
-            --  the discriminant itself, and the bounds are the culprits.
+            --  If the case is a variant part, the expression is given by the
+            --  discriminant itself, and the bounds are the culprits.
 
             if Nkind (Case_Node) = N_Variant_Part then
                Error_Msg_NE
                  ("bounds of & are not static," &
                      " alternatives must cover base type", Expr, Expr);
 
-            --  If this is a case statement, the expression may be
-            --  non-static or else the subtype may be at fault.
+            --  If this is a case statement, the expression may be non-static
+            --  or else the subtype may be at fault.
 
             elsif Is_Entity_Name (Expr) then
                Error_Msg_NE
@@ -269,30 +471,150 @@ 
          end if;
       end Explain_Non_Static_Bound;
 
-      --  Variables local to Check_Choices
+      ---------------
+      -- Lt_Choice --
+      ---------------
 
-      Choice    : Node_Id;
-      Bounds_Lo : constant Node_Id := Type_Low_Bound  (Bounds_Type);
-      Bounds_Hi : constant Node_Id := Type_High_Bound (Bounds_Type);
+      function Lt_Choice (C1, C2 : Natural) return Boolean is
+      begin
+         return
+           Expr_Value (Choice_Table (Nat (C1)).Lo)
+             <
+           Expr_Value (Choice_Table (Nat (C2)).Lo);
+      end Lt_Choice;
 
+      --------------------
+      -- Missing_Choice --
+      --------------------
+
+      procedure Missing_Choice (Value1 : Node_Id; Value2 : Node_Id) is
+      begin
+         Missing_Choice (Expr_Value (Value1), Expr_Value (Value2));
+      end Missing_Choice;
+
+      procedure Missing_Choice (Value1 : Node_Id; Value2 : Uint) is
+      begin
+         Missing_Choice (Expr_Value (Value1), Value2);
+      end Missing_Choice;
+
+      procedure Missing_Choice (Value1 : Uint; Value2 : Node_Id) is
+      begin
+         Missing_Choice (Value1, Expr_Value (Value2));
+      end Missing_Choice;
+
+      procedure Missing_Choice (Value1 : Uint; Value2 : Uint) is
+         Msg_Sloc : constant Source_Ptr := Sloc (Case_Node);
+
+      begin
+         --  AI05-0188 : within an instance the non-others choices do not have
+         --  to belong to the actual subtype.
+
+         if Ada_Version >= Ada_2012 and then In_Instance then
+            return;
+
+         --  In some situations, we call this with a null range, and obviously
+         --  we don't want to complain in this case.
+
+         elsif Value1 > Value2 then
+            return;
+         end if;
+
+         --  Case of only one value that is missing
+
+         if Value1 = Value2 then
+            if Is_Integer_Type (Bounds_Type) then
+               Error_Msg_Uint_1 := Value1;
+               Error_Msg ("missing case value: ^!", Msg_Sloc);
+            else
+               Error_Msg_Name_1 := Choice_Image (Value1, Bounds_Type);
+               Error_Msg ("missing case value: %!", Msg_Sloc);
+            end if;
+
+         --  More than one choice value, so print range of values
+
+         else
+            if Is_Integer_Type (Bounds_Type) then
+               Error_Msg_Uint_1 := Value1;
+               Error_Msg_Uint_2 := Value2;
+               Error_Msg ("missing case values: ^ .. ^!", Msg_Sloc);
+            else
+               Error_Msg_Name_1 := Choice_Image (Value1, Bounds_Type);
+               Error_Msg_Name_2 := Choice_Image (Value2, Bounds_Type);
+               Error_Msg ("missing case values: % .. %!", Msg_Sloc);
+            end if;
+         end if;
+      end Missing_Choice;
+
+      ---------------------
+      -- Missing_Choices --
+      ---------------------
+
+      procedure Missing_Choices (Pred : Node_Id; Prev_Hi : Uint) is
+         Hi  : Uint;
+         Lo  : Uint;
+         Set : Node_Id;
+
+      begin
+         Set := Pred;
+         while Present (Set) loop
+            Lo := Expr_Value (Low_Bound (Set));
+            Hi := Expr_Value (High_Bound (Set));
+
+            --  A choice covered part of a static predicate set
+
+            if Lo <= Prev_Hi and then Prev_Hi < Hi then
+               Missing_Choice (Prev_Hi + 1, Hi);
+
+            else
+               Missing_Choice (Lo, Hi);
+            end if;
+
+            Next (Set);
+         end loop;
+      end Missing_Choices;
+
+      -----------------
+      -- Move_Choice --
+      -----------------
+
+      procedure Move_Choice (From : Natural; To : Natural) is
+      begin
+         Choice_Table (Nat (To)) := Choice_Table (Nat (From));
+      end Move_Choice;
+
+      --  Local variables
+
+      Bounds_Hi     : constant Node_Id := Type_High_Bound (Bounds_Type);
+      Bounds_Lo     : constant Node_Id := Type_Low_Bound  (Bounds_Type);
+      Has_Predicate : constant Boolean :=
+                        Is_Static_Subtype (Bounds_Type)
+                          and then Present (Static_Predicate (Bounds_Type));
+      Num_Choices   : constant Nat     := Choice_Table'Last;
+
+      Choice      : Node_Id;
+      Choice_Hi   : Uint;
+      Choice_Lo   : Uint;
+      Error       : Boolean;
+      Pred        : Node_Id;
       Prev_Choice : Node_Id;
+      Prev_Lo     : Uint;
+      Prev_Hi     : Uint;
 
-      Hi      : Uint;
-      Lo      : Uint;
-      Prev_Hi : Uint;
-
    --  Start of processing for Check_Choices
 
    begin
-      --  Choice_Table must start at 0 which is an unused location used
-      --  by the sorting algorithm. However the first valid position for
-      --  a discrete choice is 1.
+      --  Choice_Table must start at 0 which is an unused location used by the
+      --  sorting algorithm. However the first valid position for a discrete
+      --  choice is 1.
 
       pragma Assert (Choice_Table'First = 0);
 
-      if Choice_Table'Last = 0 then
+      --  The choices do not cover the base range. Emit an error if "others" is
+      --  not available and return as there is no need for further processing.
+
+      if Num_Choices = 0 then
          if not Others_Present then
-            Issue_Msg (Bounds_Lo, Bounds_Hi);
+            Missing_Choice (Bounds_Lo, Bounds_Hi);
          end if;
 
          return;
@@ -300,59 +622,98 @@ 
 
       Sorting.Sort (Positive (Choice_Table'Last));
 
-      Lo      := Expr_Value (Choice_Table (1).Lo);
-      Hi      := Expr_Value (Choice_Table (1).Hi);
-      Prev_Hi := Hi;
+      --  The type covered by the list of choices is actually a static subtype
+      --  subject to a static predicate. The predicate defines subsets of legal
+      --  values and requires finer grained analysis.
 
-      if not Others_Present and then Expr_Value (Bounds_Lo) < Lo then
-         Issue_Msg (Bounds_Lo, Lo - 1);
+      if Has_Predicate then
+         Pred    := First (Static_Predicate (Bounds_Type));
+         Prev_Lo := Uint_Minus_1;
+         Prev_Hi := Uint_Minus_1;
+         Error   := False;
 
-         --  If values are missing outside of the subtype, add explanation.
-         --  No additional message if only one value is missing.
+         for Index in 1 .. Num_Choices loop
+            Check_Against_Predicate
+              (Pred    => Pred,
+               Choice  => Choice_Table (Index),
+               Prev_Lo => Prev_Lo,
+               Prev_Hi => Prev_Hi,
+               Error   => Error);
 
-         if Expr_Value (Bounds_Lo) < Lo - 1 then
-            Explain_Non_Static_Bound;
+            --  The analysis detected an illegal intersection between a choice
+            --  and a static predicate set.
+
+            if Error then
+               return;
+            end if;
+         end loop;
+
+         --  The choices may legally cover some of the static predicate sets,
+         --  but not all. Emit an error for each non-covered set.
+
+         if not Others_Present then
+            Missing_Choices (Pred, Prev_Hi);
          end if;
-      end if;
 
-      for J in 2 .. Choice_Table'Last loop
-         Lo := Expr_Value (Choice_Table (J).Lo);
-         Hi := Expr_Value (Choice_Table (J).Hi);
+      --  Default analysis
 
-         if Lo <= Prev_Hi then
-            Choice := Choice_Table (J).Node;
+      else
+         Choice_Lo := Expr_Value (Choice_Table (1).Lo);
+         Choice_Hi := Expr_Value (Choice_Table (1).Hi);
+         Prev_Hi   := Choice_Hi;
 
-            --  Find first previous choice that overlaps
+         if not Others_Present and then Expr_Value (Bounds_Lo) < Choice_Lo then
+            Missing_Choice (Bounds_Lo, Choice_Lo - 1);
 
-            for K in 1 .. J - 1 loop
-               if Lo <= Expr_Value (Choice_Table (K).Hi) then
-                  Prev_Choice := Choice_Table (K).Node;
-                  exit;
+            --  If values are missing outside of the subtype, add explanation.
+            --  No additional message if only one value is missing.
+
+            if Expr_Value (Bounds_Lo) < Choice_Lo - 1 then
+               Explain_Non_Static_Bound;
+            end if;
+         end if;
+
+         for Outer_Index in 2 .. Num_Choices loop
+            Choice_Lo := Expr_Value (Choice_Table (Outer_Index).Lo);
+            Choice_Hi := Expr_Value (Choice_Table (Outer_Index).Hi);
+
+            if Choice_Lo <= Prev_Hi then
+               Choice := Choice_Table (Outer_Index).Node;
+
+               --  Find first previous choice that overlaps
+
+               for Inner_Index in 1 .. Outer_Index - 1 loop
+                  if Choice_Lo <=
+                       Expr_Value (Choice_Table (Inner_Index).Hi)
+                  then
+                     Prev_Choice := Choice_Table (Inner_Index).Node;
+                     exit;
+                  end if;
+               end loop;
+
+               if Sloc (Prev_Choice) <= Sloc (Choice) then
+                  Error_Msg_Sloc := Sloc (Prev_Choice);
+                  Error_Msg_N ("duplication of choice value#", Choice);
+               else
+                  Error_Msg_Sloc := Sloc (Choice);
+                  Error_Msg_N ("duplication of choice value#", Prev_Choice);
                end if;
-            end loop;
 
-            if Sloc (Prev_Choice) <= Sloc (Choice) then
-               Error_Msg_Sloc := Sloc (Prev_Choice);
-               Error_Msg_N ("duplication of choice value#", Choice);
-            else
-               Error_Msg_Sloc := Sloc (Choice);
-               Error_Msg_N ("duplication of choice value#", Prev_Choice);
+            elsif not Others_Present and then Choice_Lo /= Prev_Hi + 1 then
+               Missing_Choice (Prev_Hi + 1, Choice_Lo - 1);
             end if;
 
-         elsif not Others_Present and then Lo /= Prev_Hi + 1 then
-            Issue_Msg (Prev_Hi + 1, Lo - 1);
-         end if;
+            if Choice_Hi > Prev_Hi then
+               Prev_Hi := Choice_Hi;
+            end if;
+         end loop;
 
-         if Hi > Prev_Hi then
-            Prev_Hi := Hi;
-         end if;
-      end loop;
+         if not Others_Present and then Expr_Value (Bounds_Hi) > Choice_Hi then
+            Missing_Choice (Choice_Hi + 1, Bounds_Hi);
 
-      if not Others_Present and then Expr_Value (Bounds_Hi) > Hi then
-         Issue_Msg (Hi + 1, Bounds_Hi);
-
-         if Expr_Value (Bounds_Hi) > Hi + 1 then
-            Explain_Non_Static_Bound;
+            if Expr_Value (Bounds_Hi) > Choice_Hi + 1 then
+               Explain_Non_Static_Bound;
+            end if;
          end if;
       end if;
    end Check_Choices;
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb	(revision 197743)
+++ sem_ch4.adb	(working copy)
@@ -1248,15 +1248,9 @@ 
    -----------------------------
 
    procedure Analyze_Case_Expression (N : Node_Id) is
-      Expr      : constant Node_Id := Expression (N);
-      FirstX    : constant Node_Id := Expression (First (Alternatives (N)));
-      Alt       : Node_Id;
-      Exp_Type  : Entity_Id;
-      Exp_Btype : Entity_Id;
+      function Has_Static_Predicate (Subtyp : Entity_Id) return Boolean;
+      --  Determine whether subtype Subtyp has aspect Static_Predicate
 
-      Dont_Care      : Boolean;
-      Others_Present : Boolean;
-
       procedure Non_Static_Choice_Error (Choice : Node_Id);
       --  Error routine invoked by the generic instantiation below when
       --  the case expression has a non static choice.
@@ -1270,6 +1264,28 @@ 
            Process_Associated_Node   => No_OP);
       use Case_Choices_Processing;
 
+      --------------------------
+      -- Has_Static_Predicate --
+      --------------------------
+
+      function Has_Static_Predicate (Subtyp : Entity_Id) return Boolean is
+         Item : Node_Id;
+
+      begin
+         Item := First_Rep_Item (Subtyp);
+         while Present (Item) loop
+            if Nkind (Item) = N_Aspect_Specification
+              and then Chars (Identifier (Item)) = Name_Static_Predicate
+            then
+               return True;
+            end if;
+
+            Next_Rep_Item (Item);
+         end loop;
+
+         return False;
+      end Has_Static_Predicate;
+
       -----------------------------
       -- Non_Static_Choice_Error --
       -----------------------------
@@ -1280,6 +1296,17 @@ 
            ("choice given in case expression is not static!", Choice);
       end Non_Static_Choice_Error;
 
+      --  Local variables
+
+      Expr      : constant Node_Id := Expression (N);
+      FirstX    : constant Node_Id := Expression (First (Alternatives (N)));
+      Alt       : Node_Id;
+      Exp_Type  : Entity_Id;
+      Exp_Btype : Entity_Id;
+
+      Dont_Care      : Boolean;
+      Others_Present : Boolean;
+
    --  Start of processing for Analyze_Case_Expression
 
    begin
@@ -1364,9 +1391,22 @@ 
          Exp_Type := Exp_Btype;
       end if;
 
+      --  The case expression alternatives cover the range of a static subtype
+      --  subject to aspect Static_Predicate. Do not check the choices when the
+      --  case expression has not been fully analyzed yet because this may lead
+      --  to bogus errors.
+
+      if Is_Static_Subtype (Exp_Type)
+        and then Has_Static_Predicate (Exp_Type)
+        and then In_Spec_Expression
+      then
+         null;
+
       --  Call instantiated Analyze_Choices which does the rest of the work
 
-      Analyze_Choices (N, Exp_Type, Dont_Care, Others_Present);
+      else
+         Analyze_Choices (N, Exp_Type, Dont_Care, Others_Present);
+      end if;
 
       if Exp_Type = Universal_Integer and then not Others_Present then
          Error_Msg_N
@@ -1896,10 +1936,9 @@ 
 
    begin
       A := First (Actions (N));
-      loop
+      while Present (A) loop
          Analyze (A);
          Next (A);
-         exit when No (A);
       end loop;
 
       --  This test needs a comment ???
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 197785)
+++ sem_ch13.adb	(working copy)
@@ -93,7 +93,7 @@ 
    --  the function is inserted before the freeze node, and the body of the
    --  function is inserted after the freeze node. If the predicate expression
    --  has at least one Raise_Expression, then this procedure also builds the
-   --  M version of the predicate function for ue in membership tests.
+   --  M version of the predicate function for use in membership tests.
 
    procedure Build_Static_Predicate
      (Typ  : Entity_Id;
@@ -6188,15 +6188,15 @@ 
       type REnt is record
          Lo, Hi : Uint;
       end record;
-      --  One entry in a Rlist value, a single REnt (range entry) value
-      --  denotes one range from Lo to Hi. To represent a single value
-      --  range Lo = Hi = value.
+      --  One entry in a Rlist value, a single REnt (range entry) value denotes
+      --  one range from Lo to Hi. To represent a single value range Lo = Hi =
+      --  value.
 
       type RList is array (Nat range <>) of REnt;
-      --  A list of ranges. The ranges are sorted in increasing order,
-      --  and are disjoint (there is a gap of at least one value between
-      --  each range in the table). A value is in the set of ranges in
-      --  Rlist if it lies within one of these ranges
+      --  A list of ranges. The ranges are sorted in increasing order, and are
+      --  disjoint (there is a gap of at least one value between each range in
+      --  the table). A value is in the set of ranges in Rlist if it lies
+      --  within one of these ranges.
 
       False_Range : constant RList :=
                       RList'(1 .. 0 => REnt'(No_Uint, No_Uint));
@@ -6210,41 +6210,41 @@ 
       True_Range : constant RList := RList'(1 => REnt'(BLo, BHi));
       --  Range representing True, value must be in the base range
 
-      function "and" (Left, Right : RList) return RList;
-      --  And's together two range lists, returning a range list. This is
-      --  a set intersection operation.
+      function "and" (Left : RList; Right : RList) return RList;
+      --  And's together two range lists, returning a range list. This is a set
+      --  intersection operation.
 
-      function "or" (Left, Right : RList) return RList;
-      --  Or's together two range lists, returning a range list. This is a
-      --  set union operation.
+      function "or" (Left : RList; Right : RList) return RList;
+      --  Or's together two range lists, returning a range list. This is a set
+      --  union operation.
 
       function "not" (Right : RList) return RList;
       --  Returns complement of a given range list, i.e. a range list
-      --  representing all the values in TLo .. THi that are not in the
-      --  input operand Right.
+      --  representing all the values in TLo .. THi that are not in the input
+      --  operand Right.
 
       function Build_Val (V : Uint) return Node_Id;
       --  Return an analyzed N_Identifier node referencing this value, suitable
       --  for use as an entry in the Static_Predicate list. This node is typed
       --  with the base type.
 
-      function Build_Range (Lo, Hi : Uint) return Node_Id;
-      --  Return an analyzed N_Range node referencing this range, suitable
-      --  for use as an entry in the Static_Predicate list. This node is typed
-      --  with the base type.
+      function Build_Range (Lo : Uint; Hi : Uint) return Node_Id;
+      --  Return an analyzed N_Range node referencing this range, suitable for
+      --  use as an entry in the Static_Predicate list. This node is typed with
+      --  the base type.
 
       function Get_RList (Exp : Node_Id) return RList;
-      --  This is a recursive routine that converts the given expression into
-      --  a list of ranges, suitable for use in building the static predicate.
+      --  This is a recursive routine that converts the given expression into a
+      --  list of ranges, suitable for use in building the static predicate.
 
       function Is_False (R : RList) return Boolean;
       pragma Inline (Is_False);
-      --  Returns True if the given range list is empty, and thus represents
-      --  a False list of ranges that can never be satisfied.
+      --  Returns True if the given range list is empty, and thus represents a
+      --  False list of ranges that can never be satisfied.
 
       function Is_True (R : RList) return Boolean;
-      --  Returns True if R trivially represents the True predicate by having
-      --  a single range from BLo to BHi.
+      --  Returns True if R trivially represents the True predicate by having a
+      --  single range from BLo to BHi.
 
       function Is_Type_Ref (N : Node_Id) return Boolean;
       pragma Inline (Is_Type_Ref);
@@ -6277,7 +6277,7 @@ 
       -- "and" --
       -----------
 
-      function "and" (Left, Right : RList) return RList is
+      function "and" (Left : RList; Right : RList) return RList is
          FEnt : REnt;
          --  First range of result
 
@@ -6302,8 +6302,8 @@ 
             return False_Range;
          end if;
 
-         --  Loop to remove entries at start that are disjoint, and thus
-         --  just get discarded from the result entirely.
+         --  Loop to remove entries at start that are disjoint, and thus just
+         --  get discarded from the result entirely.
 
          loop
             --  If no operands left in either operand, result is false
@@ -6328,15 +6328,15 @@ 
             end if;
          end loop;
 
-         --  Now we have two non-null operands, and first entries overlap.
-         --  The first entry in the result will be the overlapping part of
-         --  these two entries.
+         --  Now we have two non-null operands, and first entries overlap. The
+         --  first entry in the result will be the overlapping part of these
+         --  two entries.
 
          FEnt := REnt'(Lo => UI_Max (Left (SLeft).Lo, Right (SRight).Lo),
                        Hi => UI_Min (Left (SLeft).Hi, Right (SRight).Hi));
 
-         --  Now we can remove the entry that ended at a lower value, since
-         --  its contribution is entirely contained in Fent.
+         --  Now we can remove the entry that ended at a lower value, since its
+         --  contribution is entirely contained in Fent.
 
          if Left (SLeft).Hi <= Right (SRight).Hi then
             SLeft := SLeft + 1;
@@ -6344,10 +6344,10 @@ 
             SRight := SRight + 1;
          end if;
 
-         --  Compute result by concatenating this first entry with the "and"
-         --  of the remaining parts of the left and right operands. Note that
-         --  if either of these is empty, "and" will yield empty, so that we
-         --  will end up with just Fent, which is what we want in that case.
+         --  Compute result by concatenating this first entry with the "and" of
+         --  the remaining parts of the left and right operands. Note that if
+         --  either of these is empty, "and" will yield empty, so that we will
+         --  end up with just Fent, which is what we want in that case.
 
          return
            FEnt & (Left (SLeft .. Left'Last) and Right (SRight .. Right'Last));
@@ -6411,7 +6411,7 @@ 
       -- "or" --
       ----------
 
-      function "or" (Left, Right : RList) return RList is
+      function "or" (Left : RList; Right : RList) return RList is
          FEnt : REnt;
          --  First range of result
 
@@ -6436,8 +6436,8 @@ 
             return Left;
          end if;
 
-         --  Initialize result first entry from left or right operand
-         --  depending on which starts with the lower range.
+         --  Initialize result first entry from left or right operand depending
+         --  on which starts with the lower range.
 
          if Left (SLeft).Lo < Right (SRight).Lo then
             FEnt := Left (SLeft);
@@ -6447,12 +6447,12 @@ 
             SRight := SRight + 1;
          end if;
 
-         --  This loop eats ranges from left and right operands that
-         --  are contiguous with the first range we are gathering.
+         --  This loop eats ranges from left and right operands that are
+         --  contiguous with the first range we are gathering.
 
          loop
-            --  Eat first entry in left operand if contiguous or
-            --  overlapped by gathered first operand of result.
+            --  Eat first entry in left operand if contiguous or overlapped by
+            --  gathered first operand of result.
 
             if SLeft <= Left'Last
               and then Left (SLeft).Lo <= FEnt.Hi + 1
@@ -6460,8 +6460,8 @@ 
                FEnt.Hi := UI_Max (FEnt.Hi, Left (SLeft).Hi);
                SLeft := SLeft + 1;
 
-               --  Eat first entry in right operand if contiguous or
-               --  overlapped by gathered right operand of result.
+            --  Eat first entry in right operand if contiguous or overlapped by
+            --  gathered right operand of result.
 
             elsif SRight <= Right'Last
               and then Right (SRight).Lo <= FEnt.Hi + 1
@@ -6469,7 +6469,7 @@ 
                FEnt.Hi := UI_Max (FEnt.Hi, Right (SRight).Hi);
                SRight := SRight + 1;
 
-               --  All done if no more entries to eat!
+            --  All done if no more entries to eat
 
             else
                exit;
@@ -6488,20 +6488,18 @@ 
       -- Build_Range --
       -----------------
 
-      function Build_Range (Lo, Hi : Uint) return Node_Id is
+      function Build_Range (Lo : Uint; Hi : Uint) return Node_Id is
          Result : Node_Id;
+
       begin
-         if Lo = Hi then
-            return Build_Val (Hi);
-         else
-            Result :=
-              Make_Range (Loc,
-                Low_Bound  => Build_Val (Lo),
-                High_Bound => Build_Val (Hi));
-            Set_Etype (Result, Btyp);
-            Set_Analyzed (Result);
-            return Result;
-         end if;
+         Result :=
+           Make_Range (Loc,
+             Low_Bound  => Build_Val (Lo),
+             High_Bound => Build_Val (Hi));
+         Set_Etype (Result, Btyp);
+         Set_Analyzed (Result);
+
+         return Result;
       end Build_Range;
 
       ---------------
@@ -6911,11 +6909,7 @@ 
 
                   --  Convert range into required form
 
-                  if Lo = Hi then
-                     Append_To (Plist, Build_Val (Lo));
-                  else
-                     Append_To (Plist, Build_Range (Lo, Hi));
-                  end if;
+                  Append_To (Plist, Build_Range (Lo, Hi));
                end if;
             end;
          end loop;
@@ -9452,12 +9446,12 @@ 
       --  storage orders differ.
 
       if (Is_Record_Type (T1) or else Is_Array_Type (T1))
-        and then
+            and then
          (Is_Record_Type (T2) or else Is_Array_Type (T2))
         and then
          (Component_Alignment (T1) /= Component_Alignment (T2)
             or else
-          Reverse_Storage_Order (T1) /= Reverse_Storage_Order (T2))
+              Reverse_Storage_Order (T1) /= Reverse_Storage_Order (T2))
       then
          return False;
       end if;