[Ada] Spurious errors on aspect specifications in generic units

This patch fixes spurious errors on aspect specifications on record
types when the aspect expression references a component of the type that
is not a discriminant. The patch also cleans up the legality checks on
aspect specifications, and improves error message on illegal aspect
specifications whose expressions are not conformant between
specification and freeze point, because of changes in visibility.

2018-12-11  Ed Schonberg  <schonberg@adacore.com>

gcc/ada/

	* sem_ch13.adb (Push_Type, Pop_Type): New procedures, used for
	analysis of aspect expressions for record types, whose
	components (not only discriminants) may be referenced in aspect
	expressions.
	(Analyze_Aspect_Specifications, Analyze_Aspects_At_Freeze_Point,
	Analyze_Aspect_At_End-Of_Declarations,
	Resolve_Aspect_Expressions): Use the new subprograms.
	(Check_Aspect_At_End_Of_Declarations): Improve error message.
	(Build_Predicate_Functions): Do not build their bodies in a
	generic unit.
	(Is_Derived_Type_With_Constraint): New subprogram to uncover and
	reject aspect specificationss on types that appear after the
	type is frozen.
	* sem_ch13.ads (Push_Scope_And_Install_Discriminants,
	Uninstall_Discriminants_And_Pop_Scope): Remove.
	* sem_ch6.adb, sem_ch6.ads (Fully_Conformant_Expressions):
	Additional parameter to improve error message on illegal aspect
	specifications whose resolution differ between aspect
	specification and freeze point.
	* freeze.adb: Remove references to
	Install/Uninstall_Discriminants.

gcc/testsuite/

	* gnat.dg/aspect1.adb, gnat.dg/aspect1_horizontal.adb,
	gnat.dg/aspect1_horizontal.ads, gnat.dg/aspect1_vectors_2d.ads:
	New testcase.
	* gnat.dg/static_pred1.adb: Expect an error message.

From-SVN: r266980

gcc/ada/ChangeLog

+2018-12-11  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch13.adb (Push_Type, Pop_Type): New procedures, used for
+	analysis of aspect expressions for record types, whose
+	components (not only discriminants) may be referenced in aspect
+	expressions.
+	(Analyze_Aspect_Specifications, Analyze_Aspects_At_Freeze_Point,
+	Analyze_Aspect_At_End-Of_Declarations,
+	Resolve_Aspect_Expressions): Use the new subprograms.
+	(Check_Aspect_At_End_Of_Declarations): Improve error message.
+	(Build_Predicate_Functions): Do not build their bodies in a
+	generic unit.
+	(Is_Derived_Type_With_Constraint): New subprogram to uncover and
+	reject aspect specificationss on types that appear after the
+	type is frozen.
+	* sem_ch13.ads (Push_Scope_And_Install_Discriminants,
+	Uninstall_Discriminants_And_Pop_Scope): Remove.
+	* sem_ch6.adb, sem_ch6.ads (Fully_Conformant_Expressions):
+	Additional parameter to improve error message on illegal aspect
+	specifications whose resolution differ between aspect
+	specification and freeze point.
+	* freeze.adb: Remove references to
+	Install/Uninstall_Discriminants.
+
 2018-12-11  Pierre-Marie de Rodat  <derodat@adacore.com>
 
 	* doc/gnat_ugn/building_executable_programs_with_gnat.rst:

gcc/ada/freeze.adb

@@ -1938,12 +1938,6 @@ package body Freeze is
             --  for a description of how we handle aspect visibility).
 
             elsif Has_Delayed_Aspects (E) then
-
-               --  Retrieve the visibility to the discriminants in order to
-               --  analyze properly the aspects.
-
-               Push_Scope_And_Install_Discriminants (E);
-
                declare
                   Ritem : Node_Id;
 
@@ -1960,8 +1954,6 @@ package body Freeze is
                      Ritem := Next_Rep_Item (Ritem);
                   end loop;
                end;
-
-               Uninstall_Discriminants_And_Pop_Scope (E);
             end if;
 
             --  If an incomplete type is still not frozen, this may be a

gcc/ada/sem_ch13.adb

@@ -230,6 +230,23 @@ package body Sem_Ch13 is
    --  is True. This warning inserts the string Msg to describe the construct
    --  causing biasing.
 
+   -----------------------------------------------------------
+   --  Visibility of Discriminants in Aspect Specifications --
+   -----------------------------------------------------------
+
+   --  The discriminants of a type are visible when analyzing the aspect
+   --  specifications of a type declaration or protected type declaration,
+   --  but not when analyzing those of a subtype declaration. The following
+   --  routines enforce this distinction.
+
+   procedure Push_Type (E : Entity_Id);
+   --  Push scope E and make visible the discriminants of type entity E if E
+   --  has discriminants and is not a subtype.
+
+   procedure Pop_Type (E : Entity_Id);
+   --  Remove visibility to the discriminants of type entity E and pop the
+   --  scope stack if E has discriminants and is not a subtype.
+
    ---------------------------------------------------
    -- Table for Validate_Compile_Time_Warning_Error --
    ---------------------------------------------------
@@ -1353,6 +1370,13 @@ package body Sem_Ch13 is
       if May_Inherit_Delayed_Rep_Aspects (E) then
          Inherit_Delayed_Rep_Aspects (ASN);
       end if;
+
+      if In_Instance
+        and then E /= Base_Type (E)
+        and then Is_First_Subtype (E)
+      then
+         Inherit_Rep_Item_Chain (Base_Type (E), E);
+      end if;
    end Analyze_Aspects_At_Freeze_Point;
 
    -----------------------------------
@@ -5462,11 +5486,12 @@ package body Sem_Ch13 is
                   --  described in "Handling of Default and Per-Object
                   --  Expressions" in sem.ads.
 
-                  --  The visibility to the discriminants must be restored
+                  --  The visibility to the components must be established
+                  --  and restored before and after analysis.
 
-                  Push_Scope_And_Install_Discriminants (U_Ent);
+                  Push_Type (U_Ent);
                   Preanalyze_Spec_Expression (Expr, RTE (RE_CPU_Range));
-                  Uninstall_Discriminants_And_Pop_Scope (U_Ent);
+                  Pop_Type (U_Ent);
 
                   if not Is_OK_Static_Expression (Expr) then
                      Check_Restriction (Static_Priorities, Expr);
@@ -5556,14 +5581,14 @@ package body Sem_Ch13 is
                   --  described in "Handling of Default and Per-Object
                   --  Expressions" in sem.ads.
 
-                  --  The visibility to the discriminants must be restored
+                  --  The visibility to the components must be restored
 
-                  Push_Scope_And_Install_Discriminants (U_Ent);
+                  Push_Type (U_Ent);
 
                   Preanalyze_Spec_Expression
                     (Expr, RTE (RE_Dispatching_Domain));
 
-                  Uninstall_Discriminants_And_Pop_Scope (U_Ent);
+                  Pop_Type (U_Ent);
                end if;
 
             else
@@ -5644,14 +5669,14 @@ package body Sem_Ch13 is
                   --  described in "Handling of Default and Per-Object
                   --  Expressions" in sem.ads.
 
-                  --  The visibility to the discriminants must be restored
+                  --  The visibility to the components must be restored
 
-                  Push_Scope_And_Install_Discriminants (U_Ent);
+                  Push_Type (U_Ent);
 
                   Preanalyze_Spec_Expression
                     (Expr, RTE (RE_Interrupt_Priority));
 
-                  Uninstall_Discriminants_And_Pop_Scope (U_Ent);
+                  Pop_Type (U_Ent);
 
                   --  Check the No_Task_At_Interrupt_Priority restriction
 
@@ -5682,6 +5707,7 @@ package body Sem_Ch13 is
             begin
                Assoc := First (Component_Associations (Expr));
                while Present (Assoc) loop
+                  Analyze (Expression (Assoc));
                   if not Is_Entity_Name (Expression (Assoc)) then
                      Error_Msg_N ("value must be a function", Assoc);
                   end if;
@@ -5820,11 +5846,11 @@ package body Sem_Ch13 is
                   --  described in "Handling of Default and Per-Object
                   --  Expressions" in sem.ads.
 
-                  --  The visibility to the discriminants must be restored
+                  --  The visibility to the components must be restored
 
-                  Push_Scope_And_Install_Discriminants (U_Ent);
+                  Push_Type (U_Ent);
                   Preanalyze_Spec_Expression (Expr, Standard_Integer);
-                  Uninstall_Discriminants_And_Pop_Scope (U_Ent);
+                  Pop_Type (U_Ent);
 
                   if not Is_OK_Static_Expression (Expr) then
                      Check_Restriction (Static_Priorities, Expr);
@@ -8699,6 +8725,13 @@ package body Sem_Ch13 is
         or else (Present (SId) and then Has_Completion (SId))
       then
          return;
+
+        --  Do not generate predicate bodies within a generic unit. The
+        --  expressions have been analyzed already, and the bodies play
+        --  no role if not within an executable unit.
+
+      elsif Inside_A_Generic then
+         return;
       end if;
 
       --  The related type may be subject to pragma Ghost. Set the mode now to
@@ -9327,11 +9360,22 @@ package body Sem_Ch13 is
          then
             Preanalyze_Spec_Expression (End_Decl_Expr, Full_View (T));
 
+         --  The following aspect expressions may contain references to
+         --  components and discriminants of the type.
+
+         elsif A_Id  = Aspect_Dynamic_Predicate
+           or else A_Id = Aspect_Priority
+         then
+            Push_Type (Ent);
+            Preanalyze_Spec_Expression (End_Decl_Expr, T);
+            Pop_Type (Ent);
+
          else
             Preanalyze_Spec_Expression (End_Decl_Expr, T);
          end if;
 
-         Err := not Fully_Conformant_Expressions (End_Decl_Expr, Freeze_Expr);
+         Err := not Fully_Conformant_Expressions
+                 (End_Decl_Expr, Freeze_Expr, Report => True);
       end if;
 
       --  Output error message if error. Force error on aspect specification
@@ -9342,7 +9386,7 @@ package body Sem_Ch13 is
            ("!visibility of aspect for& changes after freeze point",
             ASN, Ent);
          Error_Msg_NE
-           ("info: & is frozen here, aspects evaluated at this point??",
+           ("info: & is frozen here, (RM 13.1.1 (13/3))??",
             Freeze_Node (Ent), Ent);
       end if;
    end Check_Aspect_At_End_Of_Declarations;
@@ -11193,13 +11237,9 @@ package body Sem_Ch13 is
         and then Has_Delayed_Aspects (E)
         and then Scope (E) = Current_Scope
       then
-         --  Retrieve the visibility to the discriminants in order to properly
-         --  analyze the aspects.
-
-         Push_Scope_And_Install_Discriminants (E);
-
          declare
             Ritem : Node_Id;
+            A_Id : Aspect_Id;
 
          begin
             --  Look for aspect specification entries for this entity
@@ -11210,14 +11250,26 @@ package body Sem_Ch13 is
                  and then Entity (Ritem) = E
                  and then Is_Delayed_Aspect (Ritem)
                then
-                  Check_Aspect_At_Freeze_Point (Ritem);
+                  A_Id := Get_Aspect_Id (Ritem);
+                  if A_Id = Aspect_Dynamic_Predicate
+                    or else A_Id = Aspect_Priority
+                  then
+                    --  Retrieve the visibility to components and discriminants
+                    --  in order to properly analyze the aspects.
+
+                     Push_Type (E);
+                     Check_Aspect_At_Freeze_Point (Ritem);
+                     Pop_Type (E);
+
+                  else
+                     Check_Aspect_At_Freeze_Point (Ritem);
+                  end if;
                end if;
 
                Next_Rep_Item (Ritem);
             end loop;
          end;
 
-         Uninstall_Discriminants_And_Pop_Scope (E);
       end if;
 
       --  For a record type, deal with variant parts. This has to be delayed
@@ -12402,23 +12454,33 @@ package body Sem_Ch13 is
       end if;
    end New_Stream_Subprogram;
 
-   ------------------------------------------
-   -- Push_Scope_And_Install_Discriminants --
-   ------------------------------------------
+   ---------------
+   -- Push_Type --
+   ---------------
 
-   procedure Push_Scope_And_Install_Discriminants (E : Entity_Id) is
+   procedure Push_Type (E : Entity_Id) is
+      Comp : Entity_Id;
    begin
-      if Is_Type (E) and then Has_Discriminants (E) then
+      if Ekind (E) = E_Record_Type then
          Push_Scope (E);
+         Comp := First_Component (E);
+         while Present (Comp) loop
+            Install_Entity (Comp);
+            Next_Component (Comp);
+         end loop;
 
-         --  Make the discriminants visible for type declarations and protected
-         --  type declarations, not for subtype declarations (RM 13.1.1 (12/3))
-
-         if Nkind (Parent (E)) /= N_Subtype_Declaration then
+         if Has_Discriminants (E) then
             Install_Discriminants (E);
          end if;
+
+      elsif Is_Type (E)
+         and then Has_Discriminants (E)
+         and then Nkind (Parent (E)) /= N_Subtype_Declaration
+      then
+         Push_Scope (E);
+         Install_Discriminants (E);
       end if;
-   end Push_Scope_And_Install_Discriminants;
+   end Push_Type;
 
    -----------------------------------
    -- Register_Address_Clause_Check --
@@ -12498,6 +12560,13 @@ package body Sem_Ch13 is
       S           : Entity_Id;
       Parent_Type : Entity_Id;
 
+      function Is_Derived_Type_With_Constraint return Boolean;
+      --  Check whether T is a derived type with an explicit constraint, in
+      --  which case the constraint has frozen the type and the item is too
+      --  late.  This compensates for the fact that for derived scalar types
+      --  we freeze the base type unconditionally on account of a long-standing
+      --  issue in gigi.
+
       procedure No_Type_Rep_Item;
       --  Output message indicating that no type-related aspects can be
       --  specified due to some property of the parent type.
@@ -12512,6 +12581,22 @@ package body Sem_Ch13 is
       --  document the requirement in the spec of Rep_Item_Too_Late that
       --  if True is returned, then the rep item must be completely ignored???
 
+      --------------------------------------
+      --  Is_Derived_Type_With_Constraint --
+      --------------------------------------
+
+      function Is_Derived_Type_With_Constraint return Boolean is
+         Decl : constant Node_Id := Declaration_Node (T);
+      begin
+         return Is_Derived_Type (T)
+           and then Is_Frozen (Base_Type (T))
+           and then Is_Enumeration_Type (T)
+           and then False
+           and then Nkind (N) = N_Enumeration_Representation_Clause
+           and then Nkind (Decl) = N_Subtype_Declaration
+           and then not Is_Entity_Name (Subtype_Indication (Decl));
+      end Is_Derived_Type_With_Constraint;
+
       ----------------------
       -- No_Type_Rep_Item --
       ----------------------
@@ -12541,7 +12626,9 @@ package body Sem_Ch13 is
    begin
       --  First make sure entity is not frozen (RM 13.1(9))
 
-      if Is_Frozen (T)
+      if (Is_Frozen (T)
+         or else (Is_Type (T)
+           and then Is_Derived_Type_With_Constraint))
 
         --  Exclude imported types, which may be frozen if they appear in a
         --  representation clause for a local type.
@@ -12975,9 +13062,9 @@ package body Sem_Ch13 is
    --  Start of processing for Resolve_Aspect_Expressions
 
    begin
-      --  Need to make sure discriminants, if any, are directly visible
-
-      Push_Scope_And_Install_Discriminants (E);
+      if No (ASN) then
+         return;
+      end if;
 
       while Present (ASN) loop
          if Nkind (ASN) = N_Aspect_Specification and then Entity (ASN) = E then
@@ -13004,18 +13091,19 @@ package body Sem_Ch13 is
                      --  Build predicate function specification and preanalyze
                      --  expression after type replacement. The function
                      --  declaration must be analyzed in the scope of the
-                     --  type, but the expression must see components.
+                     --  type, but the the expression can reference components
+                     --  and discriminants of the type.
 
                      if No (Predicate_Function (E)) then
-                        Uninstall_Discriminants_And_Pop_Scope (E);
                         declare
                            FDecl : constant Node_Id :=
                                      Build_Predicate_Function_Declaration (E);
                            pragma Unreferenced (FDecl);
 
                         begin
-                           Push_Scope_And_Install_Discriminants (E);
+                           Push_Type (E);
                            Resolve_Aspect_Expression (Expr);
+                           Pop_Type (E);
                         end;
                      end if;
 
@@ -13045,6 +13133,11 @@ package body Sem_Ch13 is
                      Set_Must_Not_Freeze (Expr);
                      Preanalyze_Spec_Expression (Expr, E);
 
+                  when Aspect_Priority =>
+                     Push_Type (E);
+                     Preanalyze_Spec_Expression (Expr, Any_Integer);
+                     Pop_Type (E);
+
                   --  Ditto for Storage_Size. Any other aspects that carry
                   --  expressions that should not freeze ??? This is only
                   --  relevant to the misuse of deferred constants.
@@ -13078,8 +13171,6 @@ package body Sem_Ch13 is
 
          ASN := Next_Rep_Item (ASN);
       end loop;
-
-      Uninstall_Discriminants_And_Pop_Scope (E);
    end Resolve_Aspect_Expressions;
 
    -------------------------
@@ -13586,17 +13677,24 @@ package body Sem_Ch13 is
       end if;
    end Uninstall_Discriminants;
 
-   -------------------------------------------
-   -- Uninstall_Discriminants_And_Pop_Scope --
-   -------------------------------------------
+   --------------
+   -- Pop_Type --
+   --------------
 
-   procedure Uninstall_Discriminants_And_Pop_Scope (E : Entity_Id) is
+   procedure Pop_Type (E : Entity_Id) is
    begin
-      if Is_Type (E) and then Has_Discriminants (E) then
+      if Ekind (E) = E_Record_Type and then E = Current_Scope then
+         End_Scope;
+         return;
+
+      elsif Is_Type (E)
+         and then Has_Discriminants (E)
+         and then Nkind (Parent (E)) /= N_Subtype_Declaration
+      then
          Uninstall_Discriminants (E);
          Pop_Scope;
       end if;
-   end Uninstall_Discriminants_And_Pop_Scope;
+   end Pop_Type;
 
    ------------------------------
    -- Validate_Address_Clauses --

gcc/ada/sem_ch13.ads

@@ -354,27 +354,10 @@ package Sem_Ch13 is
    --  for First, Next, and Has_Element. Optionally an Element primitive may
    --  also be defined.
 
-   -----------------------------------------------------------
-   --  Visibility of Discriminants in Aspect Specifications --
-   -----------------------------------------------------------
-
-   --  The discriminants of a type are visible when analyzing the aspect
-   --  specifications of a type declaration or protected type declaration,
-   --  but not when analyzing those of a subtype declaration. The following
-   --  routines enforce this distinction.
-
    procedure Install_Discriminants (E : Entity_Id);
    --  Make visible the discriminants of type entity E
 
-   procedure Push_Scope_And_Install_Discriminants (E : Entity_Id);
-   --  Push scope E and makes visible the discriminants of type entity E if E
-   --  has discriminants and is not a subtype.
-
    procedure Uninstall_Discriminants (E : Entity_Id);
    --  Remove visibility to the discriminants of type entity E
 
-   procedure Uninstall_Discriminants_And_Pop_Scope (E : Entity_Id);
-   --  Remove visibility to the discriminants of type entity E and pop the
-   --  scope stack if E has discriminants and is not a subtype.
-
 end Sem_Ch13;

gcc/ada/sem_ch6.adb

@@ -8823,7 +8823,8 @@ package body Sem_Ch6 is
 
    function Fully_Conformant_Expressions
      (Given_E1 : Node_Id;
-      Given_E2 : Node_Id) return Boolean
+      Given_E2 : Node_Id;
+      Report   : Boolean := False) return Boolean
    is
       E1 : constant Node_Id := Original_Node (Given_E1);
       E2 : constant Node_Id := Original_Node (Given_E2);
@@ -8831,8 +8832,12 @@ package body Sem_Ch6 is
       --  for analysis and/or expansion to make things look as though they
       --  conform when they do not, e.g. by converting 1+2 into 3.
 
-      function FCE (Given_E1, Given_E2 : Node_Id) return Boolean
-        renames Fully_Conformant_Expressions;
+      Result : Boolean;
+      function FCE (Given_E1, Given_E2 : Node_Id) return Boolean;
+      function FCE (Given_E1, Given_E2 : Node_Id) return Boolean is
+      begin
+         return Fully_Conformant_Expressions (Given_E1, Given_E2, Report);
+      end FCE;
 
       function FCL (L1, L2 : List_Id) return Boolean;
       --  Compare elements of two lists for conformance. Elements have to be
@@ -8917,6 +8922,8 @@ package body Sem_Ch6 is
    --  Start of processing for Fully_Conformant_Expressions
 
    begin
+      Result := True;
+
       --  Nonconformant if paren count does not match. Note: if some idiot
       --  complains that we don't do this right for more than 3 levels of
       --  parentheses, they will be treated with the respect they deserve.
@@ -8929,7 +8936,7 @@ package body Sem_Ch6 is
 
       elsif Is_Entity_Name (E1) and then Is_Entity_Name (E2) then
          if Present (Entity (E1)) then
-            return Entity (E1) = Entity (E2)
+            Result := Entity (E1) = Entity (E2)
 
               --  One may be a discriminant that has been replaced by the
               --  corresponding discriminal.
@@ -8968,6 +8975,14 @@ package body Sem_Ch6 is
                    and then Is_Intrinsic_Subprogram (Entity (E1))
                    and then Is_Generic_Instance (Entity (E1))
                    and then Entity (E2) = Alias (Entity (E1)));
+            if Report and not Result then
+               Error_Msg_Sloc :=
+                 Text_Ptr'Max (Sloc (Entity (E1)), Sloc (Entity (E2)));
+               Error_Msg_NE
+                 ("Meaning of& differs because of declaration#", E1, E2);
+            end if;
+
+            return Result;
 
          elsif Nkind (E1) = N_Expanded_Name
            and then Nkind (E2) = N_Expanded_Name

gcc/ada/sem_ch6.ads

@@ -172,7 +172,8 @@ package Sem_Ch6 is
 
    function Fully_Conformant_Expressions
      (Given_E1 : Node_Id;
-      Given_E2 : Node_Id) return Boolean;
+      Given_E2 : Node_Id;
+      Report   : Boolean := False) return Boolean;
    --  Determines if two (non-empty) expressions are fully conformant
    --  as defined by (RM 6.3.1(18-21))
 

gcc/testsuite/ChangeLog

+2018-12-11  Ed Schonberg  <schonberg@adacore.com>
+
+	* gnat.dg/aspect1.adb, gnat.dg/aspect1_horizontal.adb,
+	gnat.dg/aspect1_horizontal.ads, gnat.dg/aspect1_vectors_2d.ads:
+	New testcase.
+	* gnat.dg/static_pred1.adb: Expect an error message.
+
 2018-12-11  Jakub Jelinek  <jakub@redhat.com>
 
 	PR lto/86004

gcc/testsuite/gnat.dg/aspect1.adb

+--  { dg-do compile }
+
+with Aspect1_Horizontal;
+with Aspect1_Vectors_2D;
+
+procedure Aspect1 is
+   type Speed is new Float;
+   package Distances is new Aspect1_Vectors_2D (Float);
+   package Velocities is new Aspect1_Vectors_2D (Speed);
+   package Motion is new Aspect1_Horizontal (Distances, Velocities);
+begin
+   null;
+end;

gcc/testsuite/gnat.dg/aspect1_horizontal.adb

+package body Aspect1_Horizontal is
+   function Theta_D(s: Position_2d_Pkg.Vect2; nzv: Speed_2d_Pkg.Nz_vect2)
+      return float
+   is
+        a: constant float := 0.0;
+   begin
+      return 0.0;
+   end Theta_D;
+end Aspect1_Horizontal;

gcc/testsuite/gnat.dg/aspect1_horizontal.ads

+with Aspect1_Vectors_2D;
+
+generic
+   with package Position_2d_Pkg is new Aspect1_Vectors_2D (<>);
+   with package Speed_2d_Pkg is new Aspect1_Vectors_2D (<>);
+package Aspect1_Horizontal is
+   function Theta_D(s: Position_2d_Pkg.Vect2; nzv: Speed_2d_Pkg.Nz_vect2)
+      return float;
+end Aspect1_Horizontal;

gcc/testsuite/gnat.dg/aspect1_vectors_2d.ads

+generic
+   type T_horizontal is new float;
+
+-- Declaration of types, constants, and common functions on 3D vectors.
+-- Corresponds to PVS theory vectors/vectors_2D
+package Aspect1_Vectors_2D is
+
+   -- A 2D vector, represented by an x and a y coordinate.
+   type Vect2 is record
+      x: T_horizontal;
+      y: T_horizontal;
+   end record;
+
+   subtype Nz_vect2 is Vect2
+     with Predicate => (Nz_vect2.x /= 0.0 and then Nz_Vect2.y /= 0.0);
+end Aspect1_Vectors_2D;

gcc/testsuite/gnat.dg/static_pred1.adb

@@ -8,7 +8,7 @@ package body Static_Pred1 is
      Enum_Subrange in A | C;
 
    function "not" (Kind : Enum_Subrange) return Enum_Subrange is
-     (case Kind is
+     (case Kind is -- { dg-error "missing case value: \"B\"" }
       when A => C,
       when C => A);