From 442886a99dae94012575bcc1cd3407284da42081 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 31 Oct 2022 11:33:12 +0100 Subject: [PATCH] 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 | 10 +++++++--- 1 file 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; -- 2.7.4