[Ada] Move check for null array aggregates to expansion
Commit Message
Despite recent changes to runtime checks for null array aggregates,
GNATprove still struggles with N_Raise_Constraint_Error nodes inserted
into AST by aggregate resolution. The ultimate fix is to move these
checks to expansion (which is disabled in GNATprove mode) and explicitly
emit a proof check in the GNATprove backend.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* exp_aggr.adb (Check_Bounds): Move code and comment related to
check for null array aggregate from Resolve_Null_Array_Aggregate.
* sem_aggr.ads (Is_Null_Aggregate): Move spec from unit body.
* sem_aggr.adb (Resolve_Null_Array_Aggregate): Move check to
expansion.
@@ -5734,7 +5734,8 @@ package body Exp_Aggr is
procedure Check_Bounds (Aggr_Bounds_Node, Index_Bounds_Node : Node_Id);
-- Checks that the bounds of Aggr_Bounds are within the bounds defined
- -- by Index_Bounds.
+ -- by Index_Bounds. For null array aggregate (Ada 2022) check that the
+ -- aggregate bounds define a null range.
procedure Check_Same_Aggr_Bounds (Sub_Aggr : Node_Id; Dim : Pos);
-- Checks that in a multidimensional array aggregate all subaggregates
@@ -5850,6 +5851,22 @@ package body Exp_Aggr is
Cond : Node_Id := Empty;
begin
+ -- For a null array aggregate check that high bound (i.e., low
+ -- bound predecessor) exists. Fail if low bound is low bound of
+ -- base subtype (in all cases, including modular).
+
+ if Is_Null_Aggregate (N) then
+ Insert_Action (N,
+ Make_Raise_Constraint_Error (Loc,
+ Condition =>
+ Make_Op_Eq (Loc,
+ New_Copy_Tree (Aggr_Bounds.First),
+ New_Copy_Tree
+ (Type_Low_Bound (Base_Type (Etype (Ind_Bounds.First))))),
+ Reason => CE_Range_Check_Failed));
+ return;
+ end if;
+
-- Generate the following test:
-- [constraint_error when
@@ -404,10 +404,6 @@ package body Sem_Aggr is
-- The bounds of the aggregate itype are cooked up to look reasonable
-- (in this particular case the bounds will be 1 .. 2).
- function Is_Null_Aggregate (N : Node_Id) return Boolean;
- -- Returns True for a "[]" aggregate (an Ada 2022 feature), even after
- -- it has been transformed by expansion. Returns False otherwise.
-
procedure Make_String_Into_Aggregate (N : Node_Id);
-- A string literal can appear in a context in which a one dimensional
-- array of characters is expected. This procedure simply rewrites the
@@ -419,9 +415,6 @@ package body Sem_Aggr is
-- is constrained). If the subtype is unconstrained, then the bounds
-- are determined in much the same way as the bounds for a null string
-- literal with no applicable index constraint.
- -- Emit a check that the bounds for each dimension define a null
- -- range; no check is emitted if it is statically known that the
- -- check would succeed.
---------------------------------
-- Delta aggregate processing --
@@ -4102,7 +4095,6 @@ package body Sem_Aggr is
Loc : constant Source_Ptr := Sloc (N);
Typ : constant Entity_Id := Etype (N);
- Check : Node_Id;
Index : Node_Id;
Lo, Hi : Node_Id;
Constr : constant List_Id := New_List;
@@ -4127,18 +4119,6 @@ package body Sem_Aggr is
Attribute_Name => Name_Pred,
Expressions => New_List (New_Copy_Tree (Lo)));
- -- Check that high bound (i.e., low bound predecessor) exists.
- -- Fail if low bound is low bound of base subtype (in all cases,
- -- including modular).
-
- Check :=
- Make_Raise_Constraint_Error (Loc,
- Condition =>
- Make_Op_Le (Loc, New_Copy_Tree (Lo), New_Copy_Tree (Hi)),
- Reason => CE_Range_Check_Failed);
-
- Insert_Action (N, Check);
-
Append (Make_Range (Loc, New_Copy_Tree (Lo), Hi), Constr);
Analyze_And_Resolve (Last (Constr), Etype (Index));
@@ -43,6 +43,10 @@ package Sem_Aggr is
-- WARNING: There is a matching C declaration of this subprogram in fe.h
+ function Is_Null_Aggregate (N : Node_Id) return Boolean;
+ -- Returns True for a "[]" aggregate (an Ada 2022 feature), even after
+ -- it has been transformed by expansion. Returns False otherwise.
+
function Is_Null_Array_Aggregate_High_Bound (N : Node_Id) return Boolean;
-- Returns True for the high bound of a null array aggregate.