| Message ID | 20151020114929.GA119967@adacore.com |
|---|---|
| State | New |
| Headers | show |
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);
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 <kirtchev@adacore.com> * sem_ch3.adb (Analyze_Object_Contract): A protected type or a protected object is allowed to have a discriminated part.