aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/sem_util.ads
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2022-11-25 17:16:06 +0100
committerMarc Poulhiès <poulhies@adacore.com>2022-12-06 14:58:49 +0100
commit400d9fc1f04336118c3200e2af14a620e7ea1d95 (patch)
treee5b73af6d4bb71aa52f994f402185f086e2df957 /gcc/ada/sem_util.ads
parent7dc44f280e7d1126b4d05e79c53b40df1afe334a (diff)
ada: Allow No_Caching on volatile types
SPARK RM now allow the property No_Caching on volatile types, to indicate that they should be considered volatile for compilation, but not by GNATprove's analysis. gcc/ada/ * contracts.adb (Add_Contract_Item): Allow No_Caching on types. (Check_Type_Or_Object_External_Properties): Check No_Caching. Check that non-effectively volatile types does not contain an effectively volatile component (instead of just a volatile component). (Analyze_Object_Contract): Remove shared checking of No_Caching. * sem_prag.adb (Analyze_External_Property_In_Decl_Part): Adapt checking of No_Caching for types. (Analyze_Pragma): Allow No_Caching on types. * sem_util.adb (Has_Effectively_Volatile_Component): New query function. (Is_Effectively_Volatile): Type with Volatile and No_Caching is not effectively volatile. (No_Caching_Enabled): Remove assertion to apply to all entities. * sem_util.ads: Same.
Diffstat (limited to 'gcc/ada/sem_util.ads')
-rw-r--r--gcc/ada/sem_util.ads11
1 files changed, 8 insertions, 3 deletions
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 34aaa9a932f..b647e68ff7f 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1564,6 +1564,11 @@ package Sem_Util is
-- Given arbitrary expression Expr, determine whether it contains at
-- least one name whose entity is Any_Id.
+ function Has_Effectively_Volatile_Component
+ (Typ : Entity_Id) return Boolean;
+ -- Given arbitrary type Typ, determine whether it contains at least one
+ -- effectively volatile component.
+
function Has_Volatile_Component (Typ : Entity_Id) return Boolean;
-- Given arbitrary type Typ, determine whether it contains at least one
-- volatile component.
@@ -2758,9 +2763,9 @@ package Sem_Util is
-- inline this procedural form, but not the functional form above.
function No_Caching_Enabled (Id : Entity_Id) return Boolean;
- -- Given the entity of a variable, determine whether Id is subject to
- -- volatility property No_Caching and if it is, the related expression
- -- evaluates to True.
+ -- Given any entity Id, determine whether Id is subject to volatility
+ -- property No_Caching and if it is, the related expression evaluates
+ -- to True.
function No_Heap_Finalization (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ is subject to pragma No_Heap_Finalization