This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
Other format: | [Raw text] |
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.
Attachment:
difs
Description: Text document
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |