This is the mail archive of the 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] New aspect/pragma No_Caching for analysis of volatile data

A new aspect/pragma can be attached to volatile variables to indicate
that such a variable is not used for interactions with the external
world, but only that accesses to that variable should not be optimized
by the compiler. This is in particular useful for guarding against fault
injection. SPARK Reference manual has been updated to allow this use of
volatile data, see section 7.1.2, so that GNATprove can analyze such
variables as not volatile.

Tested on x86_64-pc-linux-gnu, committed on trunk

2019-08-12  Yannick Moy  <>


	* aspects.adb, (Aspect_No_Caching): New aspect.
	* contracts.adb, (Add_Contract_Item): Add handling
	of No_Caching.
	(Analyze_Object_Contract): Add handling of No_Caching.
	* einfo.adb,
	(Get_Pragma): Add handling of No_Caching.
	* doc/gnat_rm/implementation_defined_aspects.rst,
	doc/gnat_rm/implementation_defined_pragmas.rst: Document new
	* gnat_rm.texi: Regenerate.
	* par-prag.adb (Prag): New pragma Pragma_No_Caching.
	* sem_ch13.adb (Analyze_Aspect_Specifications,
	Check_Aspect_At_Freeze_Point): Add handling of No_Caching.
	* sem_prag.adb (Analyze_Pragma): Deal with pragma No_Caching.
	* (Analyze_External_Property_In_Decl_Part): Now
	applies to No_Caching.
	* sem_util.adb, (Is_Effectively_Volatile): Add
	handling of No_Caching.
	(No_Caching_Enabled): New query function.
	* New names for pragma.


	* gnat.dg/no_caching.adb, gnat.dg/ New testcase.

Attachment: patch.diff.gz
Description: application/gzip

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]