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/sem_prag.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/sem_prag.ads')
| -rw-r--r-- | gcc/ada/sem_prag.ads | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 25353b7..941a723 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -218,8 +218,9 @@ package Sem_Prag is (N : Node_Id; Expr_Val : out Boolean); -- Perform full analysis of delayed pragmas Async_Readers, Async_Writers, - -- Effective_Reads and Effective_Writes. Flag Expr_Val contains the Boolean - -- argument of the pragma or a default True if no argument is present. + -- Effective_Reads, Effective_Writes and No_Caching. Flag Expr_Val contains + -- the Boolean argument of the pragma or a default True if no argument + -- is present. procedure Analyze_Global_In_Decl_Part (N : Node_Id); -- Perform full analysis of delayed pragma Global. This routine is also |