From: Piotr Trojanek <troja...@adacore.com>
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
Tested on x86_64-pc-linux-gnu, committed on master.
---
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.43.0
