r274292 - in /trunk/gcc: ada/ChangeLog ada/aspe...

[pmderodat@gcc.gnu.org]

Author: pmderodat
Date: Mon Aug 12 08:59:53 2019
New Revision: 274292

URL: https://gcc.gnu.org/viewcvs?rev=274292&root=gcc&view=rev
Log:
[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.

2019-08-12  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* aspects.adb, aspects.ads (Aspect_No_Caching): New aspect.
	* contracts.adb, contracts.ads (Add_Contract_Item): Add handling
	of No_Caching.
	(Analyze_Object_Contract): Add handling of No_Caching.
	* einfo.adb, einfo.ads
	(Get_Pragma): Add handling of No_Caching.
	* doc/gnat_rm/implementation_defined_aspects.rst,
	doc/gnat_rm/implementation_defined_pragmas.rst: Document new
	aspect/pragma.
	* 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.
	* sem_prag.ads (Analyze_External_Property_In_Decl_Part): Now
	applies to No_Caching.
	* sem_util.adb, sem_util.ads (Is_Effectively_Volatile): Add
	handling of No_Caching.
	(No_Caching_Enabled): New query function.
	* snames.ads-tmpl: New names for pragma.

gcc/testsuite/

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

Added:
    trunk/gcc/testsuite/gnat.dg/no_caching.adb
    trunk/gcc/testsuite/gnat.dg/no_caching.ads
Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/aspects.adb
    trunk/gcc/ada/aspects.ads
    trunk/gcc/ada/contracts.adb
    trunk/gcc/ada/contracts.ads
    trunk/gcc/ada/doc/gnat_rm/implementation_defined_aspects.rst
    trunk/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
    trunk/gcc/ada/einfo.adb
    trunk/gcc/ada/einfo.ads
    trunk/gcc/ada/gnat_rm.texi
    trunk/gcc/ada/par-prag.adb
    trunk/gcc/ada/sem_ch13.adb
    trunk/gcc/ada/sem_prag.adb
    trunk/gcc/ada/sem_prag.ads
    trunk/gcc/ada/sem_util.adb
    trunk/gcc/ada/sem_util.ads
    trunk/gcc/ada/snames.ads-tmpl
    trunk/gcc/testsuite/ChangeLog