diff options
| author | Yannick Moy <moy@adacore.com> | 2019-08-12 08:59:53 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-08-12 08:59:53 +0000 |
| commit | 9dfc6c55085848a60d19825bdc0b7d345bdf8603 (patch) | |
| tree | 1aeb86d69692de5f00207e441462e5ade8f2c735 /gcc/ada/contracts.ads | |
| parent | 1debd630ed40eec6db2f4aab4524fde4643b70a7 (diff) | |
| download | gcc-9dfc6c55085848a60d19825bdc0b7d345bdf8603.zip gcc-9dfc6c55085848a60d19825bdc0b7d345bdf8603.tar.gz gcc-9dfc6c55085848a60d19825bdc0b7d345bdf8603.tar.bz2 | |
[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.
From-SVN: r274292
Diffstat (limited to 'gcc/ada/contracts.ads')
| -rw-r--r-- | gcc/ada/contracts.ads | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads index 0dc5ff9..ca99c34 100644 --- a/gcc/ada/contracts.ads +++ b/gcc/ada/contracts.ads @@ -50,6 +50,7 @@ package Contracts is -- Initial_Condition -- Initializes -- Interrupt_Handler + -- No_Caching -- Part_Of -- Postcondition -- Precondition |