This patch implements the following SPARK RM rule:
7.1.3(5) - An effectively volatile type other than a protected type shall
not have a discriminated part.
------------
-- Source --
------------
-- discrims.ads
package Discrims with SPARK_Mode is
type Vol_1 (Discr : Natural) is null record with Volatile;
type Vol_2 (Discr : Natural) is null record;
protected type Prot (Discr : Natural) is
entry E;
end Prot;
end Discrims;
-- discrims.adb
package body Discrims with SPARK_Mode is
protected body Prot is
entry E when True is begin null; end E;
end Prot;
Obj_1 : Vol_1 (1);
Obj_2 : Vol_2 (2) with Volatile;
Obj_3 : Prot (3);
Obj_4 : Prot (4) with Volatile;
end Discrims;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c discrims.adb
discrims.adb:7:04: discriminated object "Obj_2" cannot be volatile
discrims.ads:2:09: discriminated type "Vol_1" cannot be volatile
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-10-20 Hristian Kirtchev <[email protected]>
* sem_ch3.adb (Analyze_Object_Contract):
A protected type or a protected object is allowed to have a
discriminated part.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 229049)
+++ sem_ch3.adb (working copy)
@@ -3347,9 +3347,11 @@
Obj_Id);
-- An object of a discriminated type cannot be effectively
- -- volatile (SPARK RM C.6(4)).
+ -- volatile except for protected objects (SPARK RM 7.1.3(5)).
- elsif Has_Discriminants (Obj_Typ) then
+ elsif Has_Discriminants (Obj_Typ)
+ and then not Is_Protected_Type (Obj_Typ)
+ then
Error_Msg_N
("discriminated object & cannot be volatile", Obj_Id);
