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]

[Ada] Implement SPARK RM C.6 rules


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  <kirtchev@adacore.com>

	* freeze.adb (Freeze_Record_Type): Perform various
	volatility-related checks.

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]