diff options
author | Yannick Moy <moy@adacore.com> | 2022-10-31 11:33:12 +0100 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2022-11-14 14:46:50 +0100 |
commit | 442886a99dae94012575bcc1cd3407284da42081 (patch) | |
tree | f8400bd12e9b0f2854839478fa203b6d04a1b025 | |
parent | 28e5c45bd519aa363cba1eec4d215b173c360cab (diff) | |
download | gcc-442886a99dae94012575bcc1cd3407284da42081.zip gcc-442886a99dae94012575bcc1cd3407284da42081.tar.gz gcc-442886a99dae94012575bcc1cd3407284da42081.tar.bz2 |
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.
-rw-r--r-- | gcc/ada/sem_prag.adb | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 615c6d2..77fcb1c 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -23424,10 +23424,14 @@ package body Sem_Prag is Spec_Id : constant Entity_Id := Unique_Defining_Entity (Decl); begin - -- Ignore pragma when applied to the special body created for - -- inlining, recognized by its internal name _Parent. + -- Ignore pragma when applied to the special body created + -- for inlining, recognized by its internal name _Parent; or + -- when applied to the special body created for contracts, + -- recognized by its internal name _Wrapped_Statements. - if Chars (Body_Id) = Name_uParent then + if Chars (Body_Id) in Name_uParent + | Name_uWrapped_Statements + then return; end if; |