aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2022-10-31 11:33:12 +0100
committerMarc Poulhiès <poulhies@adacore.com>2022-11-14 14:46:50 +0100
commit442886a99dae94012575bcc1cd3407284da42081 (patch)
treef8400bd12e9b0f2854839478fa203b6d04a1b025
parent28e5c45bd519aa363cba1eec4d215b173c360cab (diff)
downloadgcc-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.adb10
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;