This patch implements SPARK property "effectively volatile" which states:
In SPARK 2014, the terms volatile type and volatile object are defined as
per Ada RM C.6(8/3). An effectively volatile type is a volatile type or an
array type to which the Volatile_Components aspect has been applied. An
effectively volatile object is a volatile object or an object of an array
type to which Volatile_Components has been applied.
------------
-- Source --
------------
-- volatile_comps.ads
package Volatile_Comps with SPARK_Mode is
type I is range 1 .. 10;
type VC_Array is array (I) of Integer with Volatile_Components;
type NVC_Array is array (I) of Integer;
Obj_1 : VC_Array with Async_Readers;
Obj_2 : VC_Array with Async_Readers, Effective_Reads;
Obj_3 : NVC_Array with Volatile, Async_Readers;
Obj_4 : NVC_Array with Volatile, Async_Readers, Effective_Reads;
end Volatile_Comps;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c volatile_comps.ads
volatile_comps.ads:8:04: illegal combination of external properties (SPARK RM
7.1.2(6))
volatile_comps.ads:10:04: illegal combination of external properties (SPARK RM
7.1.2(6))
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-07-31 Hristian Kirtchev <kirtc...@adacore.com>
* freeze.adb (Freeze_Record_Type): Replace all calls to
Is_SPARK_Volatile with Is_Effectively_Volatile and update
related comments.
* sem_ch3.adb (Analyze_Object_Contract, Process_Discriminants):
Replace all calls to Is_SPARK_Volatile with
Is_Effectively_Volatile and update related comments.
* sem_ch5.adb (Analyze_Iterator_Specification,
Analyze_Loop_Parameter_Specification): Replace all calls to
Is_SPARK_Volatile with Is_Effectively_Volatile and update
related comments.
* sem_ch6.adb (Process_Formals): Replace all calls to
Is_SPARK_Volatile with Is_Effectively_Volatile and update
related comments.
* sem_ch12.adb (Instantiate_Object): Replace the call to
Is_SPARK_Volatile_Object with Is_Effectively_Volatile_Object
and update related comment.
* sem_prag.adb (Analyze_External_Property_In_Decl_Part,
Analyze_Global_Item): Replace all calls to Is_SPARK_Volatile
with Is_Effectively_Volatile and update related comments.
* sem_res.adb (Resolve_Actuals, Resolve_Entity_Name): Replace
all calls to Is_SPARK_Volatile with Is_Effectively_Volatile and
update related comments.
* sem_util.adb (Has_Enabled_Property,
Variable_Has_Enabled_Property): Replace all calls
to Is_SPARK_Volatile with Is_Effectively_Volatile and
update related comments.
(Is_Effectively_Volatile): New routine.
(Is_Effectively_Volatile_Object): New routine.
(Is_SPARK_Volatile): Removed.
(Is_SPARK_Volatile_Object): Removed.
* sem_util.ads (Is_Effectively_Volatile): New routine.
(Is_Effectively_Volatile_Object): New routine.
(Is_SPARK_Volatile): Removed.
(Is_SPARK_Volatile_Object): Removed.
Index: freeze.adb
===================================================================
--- freeze.adb (revision 213350)
+++ freeze.adb (working copy)
@@ -3472,27 +3472,29 @@
-- they are not standard Ada legality rules.
if SPARK_Mode = On then
- if Is_SPARK_Volatile (Rec) then
+ if Is_Effectively_Volatile (Rec) then
- -- A discriminated type cannot be volatile (SPARK RM C.6(4))
+ -- A discriminated type cannot be effectively volatile
+ -- (SPARK RM C.6(4)).
if Has_Discriminants (Rec) then
Error_Msg_N ("discriminated type & cannot be volatile", Rec);
- -- A tagged type cannot be volatile (SPARK RM C.6(5))
+ -- A tagged type cannot be effectively volatile
+ -- (SPARK RM C.6(5)).
elsif Is_Tagged_Type (Rec) then
Error_Msg_N ("tagged type & cannot be volatile", Rec);
end if;
- -- A non-volatile record type cannot contain volatile components
- -- (SPARK RM C.6(2))
+ -- A non-effectively volatile record type cannot contain
+ -- effectively volatile components (SPARK RM C.6(2)).
else
Comp := First_Component (Rec);
while Present (Comp) loop
if Comes_From_Source (Comp)
- and then Is_SPARK_Volatile (Etype (Comp))
+ and then Is_Effectively_Volatile (Etype (Comp))
then
Error_Msg_Name_1 := Chars (Rec);
Error_Msg_N
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 213263)
+++ sem_ch12.adb (working copy)
@@ -9905,13 +9905,13 @@
("actual must exclude null to match generic formal#", Actual);
end if;
- -- A volatile object cannot be used as an actual in a generic instance.
- -- The following check is only relevant when SPARK_Mode is on as it is
- -- not a standard Ada legality rule.
+ -- An effectively volatile object cannot be used as an actual in
+ -- a generic instance. The following check is only relevant when
+ -- SPARK_Mode is on as it is not a standard Ada legality rule.
if SPARK_Mode = On
and then Present (Actual)
- and then Is_SPARK_Volatile_Object (Actual)
+ and then Is_Effectively_Volatile_Object (Actual)
then
Error_Msg_N
("volatile object cannot act as actual in generic instantiation "
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 213351)
+++ sem_ch3.adb (working copy)
@@ -3018,13 +3018,13 @@
begin
if Ekind (Obj_Id) = E_Constant then
- -- A constant cannot be volatile. This check is only relevant when
- -- SPARK_Mode is on as it is not standard Ada legality rule. Do not
- -- flag internally-generated constants that map generic formals to
- -- actuals in instantiations (SPARK RM 7.1.3(6)).
+ -- A constant cannot be effectively volatile. This check is only
+ -- relevant with SPARK_Mode on as it is not a standard Ada legality
+ -- rule. Do not flag internally-generated constants that map generic
+ -- formals to actuals in instantiations (SPARK RM 7.1.3(6)).
if SPARK_Mode = On
- and then Is_SPARK_Volatile (Obj_Id)
+ and then Is_Effectively_Volatile (Obj_Id)
and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
then
Error_Msg_N ("constant cannot be volatile", Obj_Id);
@@ -3036,37 +3036,37 @@
-- they are not standard Ada legality rules.
if SPARK_Mode = On then
- if Is_SPARK_Volatile (Obj_Id) then
+ if Is_Effectively_Volatile (Obj_Id) then
- -- The declaration of a volatile object must appear at the
- -- library level (SPARK RM 7.1.3(7), C.6(6)).
+ -- The declaration of an effectively volatile object must
+ -- appear at the library level (SPARK RM 7.1.3(7), C.6(6)).
if not Is_Library_Level_Entity (Obj_Id) then
Error_Msg_N
("volatile variable & must be declared at library level",
Obj_Id);
- -- An object of a discriminated type cannot be volatile
- -- (SPARK RM C.6(4)).
+ -- An object of a discriminated type cannot be effectively
+ -- volatile (SPARK RM C.6(4)).
elsif Has_Discriminants (Obj_Typ) then
Error_Msg_N
("discriminated object & cannot be volatile", Obj_Id);
- -- An object of a tagged type cannot be volatile
+ -- An object of a tagged type cannot be effectively volatile
-- (SPARK RM C.6(5)).
elsif Is_Tagged_Type (Obj_Typ) then
Error_Msg_N ("tagged object & cannot be volatile", Obj_Id);
end if;
- -- The object is not volatile
+ -- The object is not effectively volatile
else
- -- A non-volatile object cannot have volatile components
- -- (SPARK RM 7.1.3(7)).
+ -- A non-effectively volatile object cannot have effectively
+ -- volatile components (SPARK RM 7.1.3(7)).
- if not Is_SPARK_Volatile (Obj_Id)
+ if not Is_Effectively_Volatile (Obj_Id)
and then Has_Volatile_Component (Obj_Typ)
then
Error_Msg_N
@@ -18123,12 +18123,12 @@
end if;
end if;
- -- A discriminant cannot be volatile. This check is only relevant
- -- when SPARK_Mode is on as it is not standard Ada legality rule
- -- (SPARK RM 7.1.3(6)).
+ -- A discriminant cannot be effectively volatile. This check is only
+ -- relevant when SPARK_Mode is on as it is not standard Ada legality
+ -- rule (SPARK RM 7.1.3(6)).
if SPARK_Mode = On
- and then Is_SPARK_Volatile (Defining_Identifier (Discr))
+ and then Is_Effectively_Volatile (Defining_Identifier (Discr))
then
Error_Msg_N ("discriminant cannot be volatile", Discr);
end if;
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb (revision 213333)
+++ sem_ch5.adb (working copy)
@@ -2007,16 +2007,16 @@
end if;
end if;
- -- A loop parameter cannot be volatile. This check is peformed only
- -- when SPARK_Mode is on as it is not a standard Ada legality check
- -- (SPARK RM 7.1.3(6)).
+ -- A loop parameter cannot be effectively volatile. This check is
+ -- peformed only when SPARK_Mode is on as it is not a standard Ada
+ -- legality check (SPARK RM 7.1.3(6)).
-- Not clear whether this applies to element iterators, where the
-- cursor is not an explicit entity ???
if SPARK_Mode = On
and then not Of_Present (N)
- and then Is_SPARK_Volatile (Ent)
+ and then Is_Effectively_Volatile (Ent)
then
Error_Msg_N ("loop parameter cannot be volatile", Ent);
end if;
@@ -2732,11 +2732,11 @@
end;
end if;
- -- A loop parameter cannot be volatile. This check is peformed only
- -- when SPARK_Mode is on as it is not a standard Ada legality check
- -- (SPARK RM 7.1.3(6)).
+ -- A loop parameter cannot be effectively volatile. This check is
+ -- peformed only when SPARK_Mode is on as it is not a standard Ada
+ -- legality check (SPARK RM 7.1.3(6)).
- if SPARK_Mode = On and then Is_SPARK_Volatile (Id) then
+ if SPARK_Mode = On and then Is_Effectively_Volatile (Id) then
Error_Msg_N ("loop parameter cannot be volatile", Id);
end if;
end Analyze_Loop_Parameter_Specification;
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 213338)
+++ sem_ch6.adb (working copy)
@@ -10095,21 +10095,22 @@
("function cannot have parameter of mode `OUT` or "
& "`IN OUT`", Formal);
- -- A function cannot have a volatile formal parameter
- -- (SPARK RM 7.1.3(10)).
+ -- A function cannot have an effectively volatile formal
+ -- parameter (SPARK RM 7.1.3(10)).
- elsif Is_SPARK_Volatile (Formal) then
+ elsif Is_Effectively_Volatile (Formal) then
Error_Msg_N
("function cannot have a volatile formal parameter",
Formal);
end if;
- -- A procedure cannot have a formal parameter of mode IN because
- -- it behaves as a constant (SPARK RM 7.1.3(6)).
+ -- A procedure cannot have an effectively volatile formal
+ -- parameter of mode IN because it behaves as a constant
+ -- (SPARK RM 7.1.3(6)).
elsif Ekind (Scope (Formal)) = E_Procedure
and then Ekind (Formal) = E_In_Parameter
- and then Is_SPARK_Volatile (Formal)
+ and then Is_Effectively_Volatile (Formal)
then
Error_Msg_N
("formal parameter of mode `IN` cannot be volatile", Formal);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 213351)
+++ sem_prag.adb (working copy)
@@ -1830,16 +1830,16 @@
begin
Error_Msg_Name_1 := Pragma_Name (N);
- -- An external property pragma must apply to a volatile object other
- -- than a formal subprogram parameter (SPARK RM 7.1.3(2)). The check
- -- is performed at the end of the declarative region due to a possible
- -- out-of-order arrangement of pragmas:
+ -- An external property pragma must apply to an effectively volatile
+ -- object other than a formal subprogram parameter (SPARK RM 7.1.3(2)).
+ -- The check is performed at the end of the declarative region due to a
+ -- possible out-of-order arrangement of pragmas:
-- Obj : ...;
-- pragma Async_Readers (Obj);
-- pragma Volatile (Obj);
- if not Is_SPARK_Volatile (Obj_Id) then
+ if not Is_Effectively_Volatile (Obj_Id) then
SPARK_Msg_N
("external property % must apply to a volatile object", N);
end if;
@@ -2021,19 +2021,21 @@
-- SPARK_Mode is on as they are not standard Ada legality
-- rules.
- elsif SPARK_Mode = On and then Is_SPARK_Volatile (Item_Id) then
+ elsif SPARK_Mode = On
+ and then Is_Effectively_Volatile (Item_Id)
+ then
+ -- An effectively volatile object cannot appear as a global
+ -- item of a function (SPARK RM 7.1.3(9)).
- -- A volatile object cannot appear as a global item of a
- -- function (SPARK RM 7.1.3(9)).
-
if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
Error_Msg_NE
("volatile object & cannot act as global item of a "
& "function", Item, Item_Id);
return;
- -- A volatile object with property Effective_Reads set to
- -- True must have mode Output or In_Out.
+ -- An effectively volatile object with external property
+ -- Effective_Reads set to True must have mode Output or
+ -- In_Out.
elsif Effective_Reads_Enabled (Item_Id)
and then Global_Mode = Name_Input
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 213299)
+++ sem_res.adb (working copy)
@@ -4329,18 +4329,19 @@
-- they are not standard Ada legality rule.
if SPARK_Mode = On
- and then Is_SPARK_Volatile_Object (A)
+ and then Is_Effectively_Volatile_Object (A)
then
- -- A volatile object may act as an actual parameter when the
- -- corresponding formal is of a non-scalar volatile type.
+ -- An effectively volatile object may act as an actual
+ -- parameter when the corresponding formal is of a non-scalar
+ -- volatile type.
if Is_Volatile (Etype (F))
and then not Is_Scalar_Type (Etype (F))
then
null;
- -- A volatile object may act as an actual parameter in a call
- -- to an instance of Unchecked_Conversion.
+ -- An effectively volatile object may act as an actual
+ -- parameter in a call to an instance of Unchecked_Conversion.
elsif Is_Unchecked_Conversion_Instance (Nam) then
null;
@@ -6785,33 +6786,33 @@
Eval_Entity_Name (N);
end if;
- -- A volatile object subject to enabled properties Async_Writers or
- -- Effective_Reads must appear in a specific context. The following
- -- checks are only relevant when SPARK_Mode is on as they are not
- -- standard Ada legality rules.
+ -- An effectively volatile object subject to enabled properties
+ -- Async_Writers or Effective_Reads must appear in a specific context.
+ -- The following checks are only relevant when SPARK_Mode is on as they
+ -- are not standard Ada legality rules.
if SPARK_Mode = On
and then Is_Object (E)
- and then Is_SPARK_Volatile (E)
+ and then Is_Effectively_Volatile (E)
and then Comes_From_Source (E)
and then
(Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E))
then
- -- The volatile objects appears in a "non-interfering context" as
- -- defined in SPARK RM 7.1.3(13).
+ -- The effectively volatile objects appears in a "non-interfering
+ -- context" as defined in SPARK RM 7.1.3(13).
if Is_OK_Volatile_Context (Par, N) then
null;
- -- Assume that references to volatile objects that appear as actual
- -- parameters in a procedure call are always legal. The full legality
- -- check is done when the actuals are resolved.
+ -- Assume that references to effectively volatile objects that appear
+ -- as actual parameters in a procedure call are always legal. The
+ -- full legality check is done when the actuals are resolved.
elsif Nkind (Par) = N_Procedure_Call_Statement then
null;
-- Otherwise the context causes a side effect with respect to the
- -- volatile object.
+ -- effectively volatile object.
else
Error_Msg_N
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 213345)
+++ sem_util.adb (working copy)
@@ -7605,9 +7605,10 @@
-- Start of processing for Variable_Has_Enabled_Property
begin
- -- A non-volatile object can never possess external properties
+ -- A non-effectively volatile object can never possess external
+ -- properties.
- if not Is_SPARK_Volatile (Item_Id) then
+ if not Is_Effectively_Volatile (Item_Id) then
return False;
-- External properties related to variables come in two flavors -
@@ -7650,10 +7651,11 @@
elsif Ekind (Item_Id) = E_Variable then
return Variable_Has_Enabled_Property;
- -- Otherwise a property is enabled when the related object is volatile
+ -- Otherwise a property is enabled when the related item is effectively
+ -- volatile.
else
- return Is_SPARK_Volatile (Item_Id);
+ return Is_Effectively_Volatile (Item_Id);
end if;
end Has_Enabled_Property;
@@ -10117,6 +10119,67 @@
end if;
end Is_Descendent_Of;
+ -----------------------------
+ -- Is_Effectively_Volatile --
+ -----------------------------
+
+ function Is_Effectively_Volatile (Id : Entity_Id) return Boolean is
+ begin
+ if Is_Type (Id) then
+
+ -- An arbitrary type is effectively volatile when it is subject to
+ -- pragma Atomic or Volatile.
+
+ if Is_Volatile (Id) then
+ return True;
+
+ -- An array type is effectively volatile when it is subject to pragma
+ -- Atomic_Components or Volatile_Components or its compolent type is
+ -- effectively volatile.
+
+ elsif Is_Array_Type (Id) then
+ return
+ Has_Volatile_Components (Id)
+ or else
+ Is_Effectively_Volatile (Component_Type (Base_Type (Id)));
+
+ else
+ return False;
+ end if;
+
+ -- Otherwise Id denotes an object
+
+ else
+ return Is_Volatile (Id) or else Is_Effectively_Volatile (Etype (Id));
+ end if;
+ end Is_Effectively_Volatile;
+
+ ------------------------------------
+ -- Is_Effectively_Volatile_Object --
+ ------------------------------------
+
+ function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean is
+ begin
+ if Is_Entity_Name (N) then
+ return Is_Effectively_Volatile (Entity (N));
+
+ elsif Nkind (N) = N_Expanded_Name then
+ return Is_Effectively_Volatile (Entity (N));
+
+ elsif Nkind (N) = N_Indexed_Component then
+ return Is_Effectively_Volatile_Object (Prefix (N));
+
+ elsif Nkind (N) = N_Selected_Component then
+ return
+ Is_Effectively_Volatile_Object (Prefix (N))
+ or else
+ Is_Effectively_Volatile_Object (Selector_Name (N));
+
+ else
+ return False;
+ end if;
+ end Is_Effectively_Volatile_Object;
+
----------------------------
-- Is_Expression_Function --
----------------------------
@@ -11491,41 +11554,6 @@
end if;
end Is_SPARK_Object_Reference;
- -----------------------
- -- Is_SPARK_Volatile --
- -----------------------
-
- function Is_SPARK_Volatile (Id : Entity_Id) return Boolean is
- begin
- return Is_Volatile (Id) or else Is_Volatile (Etype (Id));
- end Is_SPARK_Volatile;
-
- ------------------------------
- -- Is_SPARK_Volatile_Object --
- ------------------------------
-
- function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean is
- begin
- if Is_Entity_Name (N) then
- return Is_SPARK_Volatile (Entity (N));
-
- elsif Nkind (N) = N_Expanded_Name then
- return Is_SPARK_Volatile (Entity (N));
-
- elsif Nkind (N) = N_Indexed_Component then
- return Is_SPARK_Volatile_Object (Prefix (N));
-
- elsif Nkind (N) = N_Selected_Component then
- return
- Is_SPARK_Volatile_Object (Prefix (N))
- or else
- Is_SPARK_Volatile_Object (Selector_Name (N));
-
- else
- return False;
- end if;
- end Is_SPARK_Volatile_Object;
-
------------------
-- Is_Statement --
------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 213345)
+++ sem_util.ads (working copy)
@@ -1171,6 +1171,15 @@
-- This is the RM definition, a type is a descendent of another type if it
-- is the same type or is derived from a descendent of the other type.
+ function Is_Effectively_Volatile (Id : Entity_Id) return Boolean;
+ -- The SPARK property "effectively volatile" applies to both types and
+ -- objects. To qualify as such, an entity must be either volatile or be
+ -- (of) an array type subject to aspect Volatile_Components.
+
+ function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean;
+ -- Determine whether an arbitrary node denotes an effectively volatile
+ -- object.
+
function Is_Expression_Function (Subp : Entity_Id) return Boolean;
-- Predicate to determine whether a scope entity comes from a rewritten
-- expression function call, and should be inlined unconditionally. Also
@@ -1310,18 +1319,6 @@
function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an object in SPARK
- function Is_SPARK_Volatile (Id : Entity_Id) return Boolean;
- -- This routine is similar to predicate Is_Volatile, but it takes SPARK
- -- semantics into account. In SPARK volatile components to not render a
- -- type volatile.
-
- function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean;
- -- Determine whether an arbitrary node denotes a volatile object reference
- -- according to the semantics of SPARK. To qualify as volatile, an object
- -- must be subject to aspect/pragma Volatile or Atomic, or have a [sub]type
- -- subject to the same attributes. Note that volatile components do not
- -- render an object volatile.
-
function Is_Statement (N : Node_Id) return Boolean;
pragma Inline (Is_Statement);
-- Check if the node N is a statement node. Note that this includes
