diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2022-09-08 14:58:24 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2022-09-26 11:02:30 +0200 |
| commit | 5549d2695a36f1cd97a1a5d2089c9c5a7f3fb03b (patch) | |
| tree | 9743f32184cb84274dedc387c4ccd5df5ed004e2 /gcc/ada/contracts.adb | |
| parent | 63055635797e98d9cc67e53c3de44bae2f4c9939 (diff) | |
| download | gcc-5549d2695a36f1cd97a1a5d2089c9c5a7f3fb03b.zip gcc-5549d2695a36f1cd97a1a5d2089c9c5a7f3fb03b.tar.gz gcc-5549d2695a36f1cd97a1a5d2089c9c5a7f3fb03b.tar.bz2 | |
ada: Only reject volatile ghost objects when SPARK_Mode is On
SPARK rule that forbids ghost volatile objects is only affecting proof
and not generation of object code. It is now only applied where SPARK_Mode
is On. This flexibility is needed to compile code automatically instrumented
by GNATcoverage.
gcc/ada/
* contracts.adb (Analyze_Object_Contract): Check SPARK_Mode before
applying SPARK rule.
Diffstat (limited to 'gcc/ada/contracts.adb')
| -rw-r--r-- | gcc/ada/contracts.adb | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 34db67a..dd573d3 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -1207,7 +1207,7 @@ package body Contracts is -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and -- SPARK RM 6.9(19)). - elsif Is_Effectively_Volatile (Obj_Id) then + elsif SPARK_Mode = On and then Is_Effectively_Volatile (Obj_Id) then Error_Msg_N ("ghost object & cannot be volatile", Obj_Id); -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)). |