This patch implements the following set of rules related to shared variables:
1. A volatile representation aspect may only be applied to an
object_declaration or a full_type_declaration.
2. A component of a non-volatile type declaration shall not be volatile.
3. A discriminant shall not be volatile.
4. Neither a discriminated type nor an object of such a type shall be
volatile.
5. Neither a tagged type nor an object of such a type shall be volatile.
6. A volatile variable shall only be declared at library-level.
------------
-- Source --
------------
-- shared_vars.ads
package Shared_Vars 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;
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;
SV2 : R7 with Volatile; -- illegal, SPARK RM C.6(5)
end Shared_Vars;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c shared_vars.ads
hared_vars.ads:8:25: entity for aspect "Volatile" must denote a full type or
object declaration
shared_vars.ads:14:07: component "F2" of non-volatile type "R2" cannot be
volatile
shared_vars.ads:17:13: discriminant cannot be volatile
shared_vars.ads:21:09: discriminated type "R4" cannot be volatile
shared_vars.ads:29:04: discriminated object "SV" cannot be volatile
shared_vars.ads:31:09: tagged type "R6" cannot be volatile
shared_vars.ads:39:04: tagged object "SV2" cannot be volatile
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-07-29 Hristian Kirtchev <kirtc...@adacore.com>
* freeze.adb (Freeze_Record_Type): Perform various
volatility-related checks.
Index: freeze.adb
===================================================================
--- freeze.adb (revision 213169)
+++ freeze.adb (working copy)
@@ -3411,6 +3411,43 @@
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 (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))
+
+ else
+ Comp := First_Component (Rec);
+ while Present (Comp) loop
+ if Comes_From_Source (Comp)
+ and then Is_SPARK_Volatile (Etype (Comp))
+ then
+ Error_Msg_Name_1 := Chars (Rec);
+ Error_Msg_N
+ ("component & of non-volatile 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
