From beb6c12a41738f6cf4a1305be6518a0955a55123 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Thu, 10 Jul 2025 12:35:47 +0200 Subject: [PATCH] ada: Only fold array attributes in SPARK when prefix is safe to evaluate Fix missing checks for prefixes of array attributes in GNATprove mode. gcc/ada/ChangeLog: * sem_attr.adb (Eval_Attribute): Only fold array attributes when prefix is static or at least safe to evaluate --- gcc/ada/sem_attr.adb | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 96029444717..f38380c381f 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -9359,6 +9359,20 @@ package body Sem_Attr is when Attribute_First => Set_Bounds; + -- In GNATprove mode we only fold array attributes when prefix is + -- static (because that's required by the Ada rules) or at least can + -- be evaluated without checks (because GNATprove would miss them). + + if GNATprove_Mode + and then + not (Static + or else (Is_Entity_Name (P) and then Is_Type (Entity (P))) + or else Statically_Names_Object (P) + or else Ekind (P_Type) = E_String_Literal_Subtype) + then + return; + end if; + if Compile_Time_Known_Value (Lo_Bound) then if Is_Real_Type (P_Type) then Fold_Ureal (N, Expr_Value_R (Lo_Bound), Static); @@ -9572,6 +9586,20 @@ package body Sem_Attr is when Attribute_Last => Set_Bounds; + -- In GNATprove mode we only fold array attributes when prefix is + -- static (because that's required by the Ada rules) or at least can + -- be evaluated without checks (because GNATprove would miss them). + + if GNATprove_Mode + and then + not (Static + or else (Is_Entity_Name (P) and then Is_Type (Entity (P))) + or else Statically_Names_Object (P) + or else Ekind (P_Type) = E_String_Literal_Subtype) + then + return; + end if; + if Compile_Time_Known_Value (Hi_Bound) then if Is_Real_Type (P_Type) then Fold_Ureal (N, Expr_Value_R (Hi_Bound), Static); @@ -9655,6 +9683,20 @@ package body Sem_Attr is Set_Bounds; + -- In GNATprove mode we only fold array attributes when prefix is + -- static (because that's required by the Ada rules) or at least can + -- be evaluated without checks (because GNATprove would miss them). + + if GNATprove_Mode + and then + not (Static + or else (Is_Entity_Name (P) and then Is_Type (Entity (P))) + or else Statically_Names_Object (P) + or else Ekind (P_Type) = E_String_Literal_Subtype) + then + return; + end if; + -- For two compile time values, we can compute length if Compile_Time_Known_Value (Lo_Bound) -- 2.47.2