https://gcc.gnu.org/g:beb6c12a41738f6cf4a1305be6518a0955a55123
commit r16-2419-gbeb6c12a41738f6cf4a1305be6518a0955a55123
Author: Piotr Trojanek <troja...@adacore.com>
Date: Thu Jul 10 12:35:47 2025 +0200
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
Diff:
---
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 960294447172..f38380c381f6 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)
