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/objc | |
| 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/objc')
0 files changed, 0 insertions, 0 deletions