| commit | 5549d2695a36f1cd97a1a5d2089c9c5a7f3fb03b | |
| author | Piotr Trojanek <trojanek@adacore.com> | |
| Thu, 8 Sep 2022 12:58:24 +0000 (8 14:58 +0200) | ||
| committer | Marc Poulhiès <poulhies@adacore.com> | |
| Mon, 26 Sep 2022 09:02:30 +0000 (26 11:02 +0200) | ||
| tree | 9743f32184cb84274dedc387c4ccd5df5ed004e2 | treesnapshot (tar.gz zip) |
| parent | 63055635797e98d9cc67e53c3de44bae2f4c9939 | commitdiff |
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.
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.
| gcc/ada/contracts.adb | diffblobblamehistory |