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.adb | |
| 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.adb')
| -rw-r--r-- | gcc/ada/contracts.adb | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 4610b53..981bb91 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -317,6 +317,7 @@ package body Contracts is -- Effective_Reads -- Effective_Writes -- Global + -- No_Caching -- Part_Of elsif Ekind (Id) = E_Variable then @@ -327,6 +328,7 @@ package body Contracts is Name_Effective_Reads, Name_Effective_Writes, Name_Global, + Name_No_Caching, Name_Part_Of) then Add_Classification; @@ -741,6 +743,7 @@ package body Contracts is AW_Val : Boolean := False; ER_Val : Boolean := False; EW_Val : Boolean := False; + NC_Val : Boolean := False; Items : Node_Id; Prag : Node_Id; Ref_Elmt : Elmt_Id; @@ -847,6 +850,14 @@ package body Contracts is Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); end if; + -- Analyze the non-external volatility property No_Caching + + Prag := Get_Pragma (Obj_Id, Pragma_No_Caching); + + if Present (Prag) then + Analyze_External_Property_In_Decl_Part (Prag, NC_Val); + end if; + -- The anonymous object created for a single concurrent type carries -- pragmas Depends and Globat of the type. |