]> git.ipfire.org Git - thirdparty/gcc.git/commit
projects / thirdparty / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6305563) | patch
ada: Only reject volatile ghost objects when SPARK_Mode is On
authorPiotr Trojanek <trojanek@adacore.com>
Thu, 8 Sep 2022 12:58:24 +0000 (14:58 +0200)
committerMarc Poulhiès <poulhies@adacore.com>
Mon, 26 Sep 2022 09:02:30 +0000 (11:02 +0200)
commit5549d2695a36f1cd97a1a5d2089c9c5a7f3fb03b
tree9743f32184cb84274dedc387c4ccd5df5ed004e2tree
parent63055635797e98d9cc67e53c3de44bae2f4c9939commit | diff
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.
gcc/ada/contracts.adb diff | blob | blame | history
Mirror of https://gcc.gnu.org/git/gcc.git