This patch implements the rules defined in SPARK 2014 RM section C.6. The rules
forbit certain constructs to be labelled as volatile.
------------
-- Source --
------------
-- shared_variables.ads
package Shared_Variables
with SPARK_Mode => On
is
type T is new Integer
with Volatile; -- OK
type Colour is (Red, Green, Blue)
with Volatile; -- OK
S : Integer
with Volatile; -- OK
type R is record
F1 : Integer;
F2 : Integer with Volatile; -- illegal, SPARK RM C.6(1)
F3 : Boolean;
end record;
type R2 is record
F1 : Integer;
F2 : T; -- illegal, SPARK RM C.6(2)
end record;
type R3 (D : Colour) is record -- illegal, SPARK RM C.6(3)
Intensity : Natural;
end record;
type R4 (D : Boolean) is record
F1 : Integer;
end record with Volatile; -- illegal, SPARK RM C.6(4)
type R5 (D : Boolean := False) is record
F1 : Integer;
end record; -- legal
SV : R5 with Volatile; -- illegal, SPARK RM C.6(4)
type R6 is tagged record
F1 : Integer;
end record with Volatile; -- illegal, SPARK RM C.6(5)
type R7 is tagged record
F1 : Integer;
end record; -- legal
SV2 : R7 with Volatile; -- illegal, SPARK RM C.6(5)
end Shared_Variables;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c shared_variables.ads
shared_variables.ads:15:07: component "F2" of non-volatile record type "R"
cannot be volatile
shared_variables.ads:15:25: argument of aspect "Volatile" must denote a full
type or object declaration
shared_variables.ads:21:07: component "F2" of non-volatile record type "R2"
cannot be volatile
shared_variables.ads:24:13: discriminant cannot be volatile
shared_variables.ads:28:09: discriminated type "R4" cannot be volatile
shared_variables.ads:36:04: discriminated object "SV" cannot be volatile
shared_variables.ads:38:09: tagged type "R6" cannot be volatile
shared_variables.ads:46:04: tagged object "SV2" cannot be volatile
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-05-21 Hristian Kirtchev <[email protected]>
* freeze.adb (Freeze_Record_Type): Ensure that a discriminated
or a tagged type is not labelled as volatile. Ensure that a
non-volatile type has no volatile components.
* sem_ch3.adb (Analyze_Object_Contract): Add local constant
Obj_Typ. Code reformatting. Ensure that a discriminated or
tagged object is not labelled as volatile.
* sem_prag.adb (Process_Atomic_Shared_Volatile): Ensure that
pragma Volatile applies to a full type declaration or an object
declaration when SPARK mode is on.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 210695)
+++ sem_ch3.adb (working copy)
@@ -2980,12 +2980,13 @@
-----------------------------
procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
- AR_Val : Boolean := False;
- AW_Val : Boolean := False;
- ER_Val : Boolean := False;
- EW_Val : Boolean := False;
- Prag : Node_Id;
- Seen : Boolean := False;
+ Obj_Typ : constant Entity_Id := Etype (Obj_Id);
+ AR_Val : Boolean := False;
+ AW_Val : Boolean := False;
+ ER_Val : Boolean := False;
+ EW_Val : Boolean := False;
+ Prag : Node_Id;
+ Seen : Boolean := False;
begin
if Ekind (Obj_Id) = E_Constant then
@@ -3008,26 +3009,43 @@
-- they are not standard Ada legality rules.
if SPARK_Mode = On then
+ if Is_SPARK_Volatile_Object (Obj_Id) then
- -- A non-volatile object cannot have volatile components
- -- (SPARK RM 7.1.3(7)).
+ -- The declaration of a volatile object must appear at the
+ -- library level (SPARK RM 7.1.3(7), C.6(6)).
- if not Is_SPARK_Volatile_Object (Obj_Id)
- and then Has_Volatile_Component (Etype (Obj_Id))
- then
- Error_Msg_N
- ("non-volatile variable & cannot have volatile components",
- Obj_Id);
+ if not Is_Library_Level_Entity (Obj_Id) then
+ Error_Msg_N
+ ("volatile variable & must be declared at library level",
+ Obj_Id);
- -- The declaration of a volatile object must appear at the library
- -- level.
+ -- An object of a discriminated type cannot be volatile
+ -- (SPARK RM C.6(4)).
- elsif Is_SPARK_Volatile_Object (Obj_Id)
- and then not Is_Library_Level_Entity (Obj_Id)
- then
- Error_Msg_N
- ("volatile variable & must be declared at library level "
- & "(SPARK RM 7.1.3(5))", Obj_Id);
+ 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
+ -- (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
+
+ else
+ -- A non-volatile object cannot have volatile components
+ -- (SPARK RM 7.1.3(7)).
+
+ if not Is_SPARK_Volatile_Object (Obj_Id)
+ and then Has_Volatile_Component (Obj_Typ)
+ then
+ Error_Msg_N
+ ("non-volatile object & cannot have volatile components",
+ Obj_Id);
+ end if;
end if;
end if;
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 210690)
+++ sem_prag.adb (working copy)
@@ -6387,6 +6387,21 @@
Error_Pragma_Arg
("inappropriate entity for pragma%", Arg1);
end if;
+
+ -- The following check are only relevant when SPARK_Mode is on as
+ -- those are not a standard Ada legality rule. Pragma Volatile can
+ -- only apply to a full type declaration or an object declaration
+ -- (SPARK RM C.6(1)).
+
+ if SPARK_Mode = On
+ and then Prag_Id = Pragma_Volatile
+ and then not Nkind_In (K, N_Full_Type_Declaration,
+ N_Object_Declaration)
+ then
+ Error_Pragma_Arg
+ ("argument of pragma % must denote a full type or object "
+ & "declaration", Arg1);
+ end if;
end Process_Atomic_Shared_Volatile;
-------------------------------------------
Index: freeze.adb
===================================================================
--- freeze.adb (revision 210695)
+++ freeze.adb (working copy)
@@ -3314,6 +3314,45 @@
end if;
end if;
+ -- The following checks are only relevant when SPARK_Mode is on as
+ -- they are not standard Ada legality rules.
+
+ if SPARK_Mode = On then
+ if Is_SPARK_Volatile_Object (Rec) then
+
+ -- A discriminated type cannot be 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))
+
+ 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)). The check is performed at freeze point
+ -- because the volatility status of the record type and its
+ -- components is clearly known.
+
+ else
+ Comp := First_Component (Rec);
+ while Present (Comp) loop
+ if Comes_From_Source (Comp)
+ and then Is_SPARK_Volatile_Object (Comp)
+ then
+ Error_Msg_Name_1 := Chars (Rec);
+ Error_Msg_N
+ ("component & of non-volatile record type % cannot be "
+ & "volatile", Comp);
+ end if;
+
+ Next_Component (Comp);
+ end loop;
+ end if;
+ end if;
+
-- All done if not a full record definition
if Ekind (Rec) /= E_Record_Type then
