From: Yannick Moy <moy@adacore.com>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/contracts.adb | 32 ++++++++++++++--------------
gcc/ada/sem_prag.adb | 49 +++++++++++++++++++++++--------------------
gcc/ada/sem_util.adb | 37 +++++++++++++++++++++++++++++---
gcc/ada/sem_util.ads | 11 +++++++---
4 files changed, 84 insertions(+), 45 deletions(-)
@@ -316,6 +316,7 @@ package body Contracts is
| Name_Async_Writers
| Name_Effective_Reads
| Name_Effective_Writes
+ | Name_No_Caching
or else (Ekind (Id) = E_Task_Type
and Prag_Nam in Name_Part_Of
| Name_Depends
@@ -859,6 +860,7 @@ package body Contracts is
AW_Val : Boolean := False;
ER_Val : Boolean := False;
EW_Val : Boolean := False;
+ NC_Val : Boolean;
Seen : Boolean := False;
Prag : Node_Id;
Obj_Typ : Entity_Id;
@@ -956,18 +958,25 @@ package body Contracts is
end if;
-- Verify the mutual interaction of the various external properties.
- -- For variables for which No_Caching is enabled, it has been checked
- -- already that only False values for other external properties are
- -- allowed.
+ -- For types and variables for which No_Caching is enabled, it has been
+ -- checked already that only False values for other external properties
+ -- are allowed.
if Seen
- and then (Ekind (Type_Or_Obj_Id) /= E_Variable
- or else not No_Caching_Enabled (Type_Or_Obj_Id))
+ and then not No_Caching_Enabled (Type_Or_Obj_Id)
then
Check_External_Properties
(Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
end if;
+ -- Analyze the non-external volatility property No_Caching
+
+ Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_No_Caching);
+
+ if Present (Prag) then
+ Analyze_External_Property_In_Decl_Part (Prag, NC_Val);
+ end if;
+
-- The following checks are relevant only when SPARK_Mode is on, as
-- they are not standard Ada legality rules. Internally generated
-- temporaries are ignored, as well as return objects.
@@ -1047,10 +1056,10 @@ package body Contracts is
if Is_Type_Id
and then not Is_Effectively_Volatile (Type_Or_Obj_Id)
- and then Has_Volatile_Component (Type_Or_Obj_Id)
+ and then Has_Effectively_Volatile_Component (Type_Or_Obj_Id)
then
Error_Msg_N
- ("non-volatile type & cannot have volatile"
+ ("non-volatile type & cannot have effectively volatile"
& " components",
Type_Or_Obj_Id);
end if;
@@ -1076,7 +1085,6 @@ package body Contracts is
Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
-- Save the SPARK_Mode-related data to restore on exit
- NC_Val : Boolean;
Items : Node_Id;
Prag : Node_Id;
Ref_Elmt : Elmt_Id;
@@ -1118,14 +1126,6 @@ package body Contracts is
Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id => Obj_Id);
- -- Analyze the non-external volatility property No_Caching
-
- Prag := Get_Pragma (Obj_Id, Pragma_No_Caching);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, NC_Val);
- end if;
-
-- Constant-related checks
if Ekind (Obj_Id) = E_Constant then
@@ -2116,9 +2116,16 @@ package body Sem_Prag is
First (Pragma_Argument_Associations (N));
Obj_Decl : constant Node_Id := Find_Related_Context (N);
Obj_Id : constant Entity_Id := Defining_Entity (Obj_Decl);
+ Obj_Typ : Entity_Id;
Expr : Node_Id;
begin
+ if Is_Type (Obj_Id) then
+ Obj_Typ := Obj_Id;
+ else
+ Obj_Typ := Etype (Obj_Id);
+ end if;
+
-- Ensure that the Boolean expression (if present) is static. A missing
-- argument defaults the value to True (SPARK RM 7.1.2(5)).
@@ -2153,9 +2160,7 @@ package body Sem_Prag is
if Prag_Id /= Pragma_No_Caching
and then not Is_Effectively_Volatile (Obj_Id)
then
- if Ekind (Obj_Id) = E_Variable
- and then No_Caching_Enabled (Obj_Id)
- then
+ if No_Caching_Enabled (Obj_Id) then
if Expr_Val then -- Confirming value of False is allowed
SPARK_Msg_N
("illegal combination of external property % and property "
@@ -2167,15 +2172,16 @@ package body Sem_Prag is
N);
end if;
- -- Pragma No_Caching should only apply to volatile variables of
+ -- Pragma No_Caching should only apply to volatile types or variables of
-- a non-effectively volatile type (SPARK RM 7.1.2).
elsif Prag_Id = Pragma_No_Caching then
- if Is_Effectively_Volatile (Etype (Obj_Id)) then
- SPARK_Msg_N ("property % must not apply to an object of "
+ if Is_Effectively_Volatile (Obj_Typ) then
+ SPARK_Msg_N ("property % must not apply to a type or object of "
& "an effectively volatile type", N);
elsif not Is_Volatile (Obj_Id) then
- SPARK_Msg_N ("property % must apply to a volatile object", N);
+ SPARK_Msg_N
+ ("property % must apply to a volatile type or object", N);
end if;
end if;
@@ -13484,22 +13490,19 @@ package body Sem_Prag is
Obj_Or_Type_Decl := Find_Related_Context (N, Do_Checks => True);
-- Pragma must apply to a object declaration or to a type
- -- declaration (only the former in the No_Caching case).
- -- Original_Node is necessary to account for untagged derived
- -- types that are rewritten as subtypes of their
- -- respective root types.
-
- if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration then
- if Prag_Id = Pragma_No_Caching
- or else Nkind (Original_Node (Obj_Or_Type_Decl)) not in
- N_Full_Type_Declaration |
- N_Private_Type_Declaration |
- N_Formal_Type_Declaration |
- N_Task_Type_Declaration |
- N_Protected_Type_Declaration
- then
- Pragma_Misplaced;
- end if;
+ -- declaration. Original_Node is necessary to account for
+ -- untagged derived types that are rewritten as subtypes of
+ -- their respective root types.
+
+ if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration
+ and then Nkind (Original_Node (Obj_Or_Type_Decl)) not in
+ N_Full_Type_Declaration |
+ N_Private_Type_Declaration |
+ N_Formal_Type_Declaration |
+ N_Task_Type_Declaration |
+ N_Protected_Type_Declaration
+ then
+ Pragma_Misplaced;
end if;
Obj_Or_Type_Id := Defining_Entity (Obj_Or_Type_Decl);
@@ -13530,6 +13530,36 @@ package body Sem_Util is
return Has_Undef_Ref;
end Has_Undefined_Reference;
+ ----------------------------------------
+ -- Has_Effectively_Volatile_Component --
+ ----------------------------------------
+
+ function Has_Effectively_Volatile_Component
+ (Typ : Entity_Id) return Boolean
+ is
+ Comp : Entity_Id;
+
+ begin
+ if Has_Volatile_Components (Typ) then
+ return True;
+
+ elsif Is_Array_Type (Typ) then
+ return Is_Effectively_Volatile (Component_Type (Typ));
+
+ elsif Is_Record_Type (Typ) then
+ Comp := First_Component (Typ);
+ while Present (Comp) loop
+ if Is_Effectively_Volatile (Etype (Comp)) then
+ return True;
+ end if;
+
+ Next_Component (Comp);
+ end loop;
+ end if;
+
+ return False;
+ end Has_Effectively_Volatile_Component;
+
----------------------------
-- Has_Volatile_Component --
----------------------------
@@ -16663,9 +16693,11 @@ package body Sem_Util is
if Is_Type (Id) then
-- An arbitrary type is effectively volatile when it is subject to
- -- pragma Atomic or Volatile.
+ -- pragma Atomic or Volatile, unless No_Caching is enabled.
- if Is_Volatile (Id) then
+ if Is_Volatile (Id)
+ and then not No_Caching_Enabled (Id)
+ then
return True;
-- An array type is effectively volatile when it is subject to pragma
@@ -24579,7 +24611,6 @@ package body Sem_Util is
------------------------
function No_Caching_Enabled (Id : Entity_Id) return Boolean is
- pragma Assert (Ekind (Id) = E_Variable);
Prag : constant Node_Id := Get_Pragma (Id, Pragma_No_Caching);
Arg1 : Node_Id;
@@ -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