projects / platform / upstream / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 28e5c45) | patch
ada: Fix error on SPARK_Mode on library-level separate body
authorYannick Moy <moy@adacore.com>
Mon, 31 Oct 2022 10:33:12 +0000 (11:33 +0100)
committerMarc Poulhiès <poulhies@adacore.com>
Mon, 14 Nov 2022 13:46:50 +0000 (14:46 +0100)
commit442886a99dae94012575bcc1cd3407284da42081
treef8400bd12e9b0f2854839478fa203b6d04a1b025tree | snapshot
parent28e5c45bd519aa363cba1eec4d215b173c360cabcommit | diff
ada: Fix error on SPARK_Mode on library-level separate body

When applying explicitly SPARK_Mode on a separate library-level spec
and body for which a contract needs to be checked, compilation with
-gnata was failing on a spurious error related to SPARK_Mode
placement. Now fixed.

gcc/ada/

* sem_prag.adb (Analyze_Pragma): Add special case for the special
local subprogram created for contracts.
gcc/ada/sem_prag.adb diff | blob | history
Domain: System / Toolchain;