From patchwork Thu Aug 3 12:09:07 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 130535 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:9f41:0:b0:3e4:2afc:c1 with SMTP id v1csp1102685vqx; Thu, 3 Aug 2023 05:11:30 -0700 (PDT) X-Google-Smtp-Source: APBJJlHuxul4QSsKgw2B2YcEctQEumGAxuqon3QIPTY/vjSiAU+FADX3LCuCbV+/QrGdG+7lmT3t X-Received: by 2002:a05:6512:472:b0:4fd:fadc:f1e with SMTP id x18-20020a056512047200b004fdfadc0f1emr7228459lfd.44.1691064690552; Thu, 03 Aug 2023 05:11:30 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1691064690; cv=none; d=google.com; s=arc-20160816; b=HxGVFz/D6UvbEV2xfVsltPNkdVyv+iH81Cq+8AvvLBAoaJZf7Ik1cM/86e0iFxH8qD qbaRD+3QrCaCM5ZIDkwvx4KYi5N92cvTU8xn+ITZ0lHDVd6GdqYjph1gjjU9MN4QrB5/ A4WyMp0yrmHZRM+VKln2iHCKUTpI495XIQuK6J+rdunWYDrjOQj+Owhwz1G66E3BJFsA PIHIj1Kpm7bFXCFI3r3jYjyIJ1aL2iw8Ft3kRM8/9OBdRW7cI8EHungu2PCpoQuLvpOV w5EfILvNPSPlRIiImau0CmxhuIufBHDu/gBYH2agcsvTHguoL7IR+R8yiQWvsepNbOcx wtJw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:reply-to:from:list-subscribe:list-help:list-post :list-archive:list-unsubscribe:list-id:precedence :content-transfer-encoding:mime-version:message-id:date:subject:cc :to:dmarc-filter:delivered-to:dkim-signature:dkim-filter; bh=U27CQkxc+kELvVz9kZrebr2u6oeQ8o98ofWawQpbUwA=; fh=IG1vP+QW/+W8mciGx+F2QUKHSqhPuxx3asUj+NTFqQw=; b=qrpi7vMXa9zp+UXAlUqmgh+hy+ikMZaiWpeRkozQ+cGEBxIPshjr4KdazmmLdTroHa KuAd9gnuLKHO5t1GiAqMpIwIpKlDEivvr94CS2lXkGXOL/MjG9XocmbIf617kgJluiec /J8DtS4jzqCpGR2p059FNVMBSbrM96QhCuTzb5SIuOZPDllnf+1u2y3kAbwhYsvMmXL2 x/4J/7w/b7wEqqfTCIiiVOcoRVTfmnFlFDcNf9CU9rPrZuUFAbHWW0F4qu684ybw5xZH D0vkKaG8CMubcvf2r1RsBMqk8PQuknalQFcAmoGFrnPQHANQsGuL4vdn4jjehSs8DZbR 86uw== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=d7nC9Svc; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from server2.sourceware.org (ip-8-43-85-97.sourceware.org. [8.43.85.97]) by mx.google.com with ESMTPS id f8-20020a50ee88000000b005222ae088b1si106946edr.271.2023.08.03.05.11.30 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 03 Aug 2023 05:11:30 -0700 (PDT) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) client-ip=8.43.85.97; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=d7nC9Svc; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id C6D633857028 for ; Thu, 3 Aug 2023 12:10:50 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org C6D633857028 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1691064650; bh=U27CQkxc+kELvVz9kZrebr2u6oeQ8o98ofWawQpbUwA=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=d7nC9SvcBG4PP3bOTN7iz/1Wj9kA3z+HTb67/KpacSvE+UpFKSuvzEfp1xmKovrkd rcvsYL30UzllU3yp3tdm5oVD0lIQhHx0DjMn00nA6Nnt4ZQpc0rjKYHojbOTKh+MQ1 R81Yl0fdUHD2nALhXvxC+cMmF0eR3xZTS5aQtOdY= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x32f.google.com (mail-wm1-x32f.google.com [IPv6:2a00:1450:4864:20::32f]) by sourceware.org (Postfix) with ESMTPS id 5BB7C3856DCB for ; Thu, 3 Aug 2023 12:09:10 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 5BB7C3856DCB Received: by mail-wm1-x32f.google.com with SMTP id 5b1f17b1804b1-3fe1a17f983so8769135e9.3 for ; Thu, 03 Aug 2023 05:09:10 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1691064549; x=1691669349; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=U27CQkxc+kELvVz9kZrebr2u6oeQ8o98ofWawQpbUwA=; b=ObqRnOlm44CGYDiBSj4cpPdOt+Kn3Enk4rnWkw5D7erldU+rTjX5ndAhuDdy3BEGz6 PK67lPLtsZczYVVMPCPfIh5RmWwSigUglOyYe7ZH1y9x9gv0XdMhbZpRIXtpeAPSUl9b Fh83U+1AWJ8t2ltCsdkkkz7CaDPp1xS7td7ADiKhFsnsRW9HBG7ioqXH2Rder1SB14gu T+xvGZgJx0d0XA92muLr52CPrSXdUmsBFgL5HQg8OTeXAIu3Dw7r/SSWTTOBZRYJhtbX Tji2JnAxtWUnxbmtib/HHfd/5mze6XSgyrB1lCF+jkEEbu5gsHjUd29rJ0XIj7z6T+QB 03pw== X-Gm-Message-State: ABy/qLYauZ0RYZTel1opv3kmkLp6cXv2UBky0nvUnzuhFkykjuJrDtbQ 9MuSENPUVeu6J+5No4HVpzDu8fOAtHNH90sGMXwMHw== X-Received: by 2002:a7b:cd8a:0:b0:3fe:2b8c:9f0b with SMTP id y10-20020a7bcd8a000000b003fe2b8c9f0bmr5116873wmj.23.1691064549114; Thu, 03 Aug 2023 05:09:09 -0700 (PDT) Received: from poulhies-Precision-5550.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id l7-20020adfe587000000b00314172ba213sm21756974wrm.108.2023.08.03.05.09.08 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 03 Aug 2023 05:09:08 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Sheri Bernstein Subject: [COMMITTED] ada: Add pragma Annotate for GNATcheck exemptions Date: Thu, 3 Aug 2023 14:09:07 +0200 Message-Id: <20230803120907.2526791-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.3 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: =?utf-8?q?Marc_Poulhi=C3=A8s_via_Gcc-patches?= From: =?utf-8?q?Marc_Poulhi=C3=A8s?= Reply-To: =?utf-8?q?Marc_Poulhi=C3=A8s?= Errors-To: gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org Sender: "Gcc-patches" X-getmail-retrieved-from-mailbox: INBOX X-GMAIL-THRID: 1773209848951841288 X-GMAIL-MSGID: 1773209848951841288 From: Sheri Bernstein Exempt the GNATcheck rule "Improper_Returns" with the rationale "early returns for performance". gcc/ada/ * libgnat/s-aridou.adb: Add pragma to exempt Improper_Returns. * libgnat/s-atopri.adb (Lock_Free_Try_Write): Likewise. * libgnat/s-bitops.adb (Bit_Eq): Likewise. * libgnat/s-carsi8.adb: Likewise. * libgnat/s-carun8.adb: Likewise. * libgnat/s-casi16.adb: Likewise. * libgnat/s-casi32.adb: Likewise. * libgnat/s-casi64.adb: Likewise. * libgnat/s-caun16.adb: Likewise. * libgnat/s-caun32.adb: Likewise. * libgnat/s-caun64.adb: Likewise. * libgnat/s-exponn.adb: Likewise. * libgnat/s-expont.adb: Likewise. * libgnat/s-valspe.adb: Likewise. * libgnat/s-vauspe.adb: Likewise. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/s-aridou.adb | 4 ++++ gcc/ada/libgnat/s-atopri.adb | 5 +++++ gcc/ada/libgnat/s-bitops.adb | 5 +++++ gcc/ada/libgnat/s-carsi8.adb | 4 ++++ gcc/ada/libgnat/s-carun8.adb | 4 ++++ gcc/ada/libgnat/s-casi16.adb | 4 ++++ gcc/ada/libgnat/s-casi32.adb | 4 ++++ gcc/ada/libgnat/s-casi64.adb | 4 ++++ gcc/ada/libgnat/s-caun16.adb | 4 ++++ gcc/ada/libgnat/s-caun32.adb | 4 ++++ gcc/ada/libgnat/s-caun64.adb | 4 ++++ gcc/ada/libgnat/s-exponn.adb | 5 +++++ gcc/ada/libgnat/s-expont.adb | 5 +++++ gcc/ada/libgnat/s-valspe.adb | 5 +++++ gcc/ada/libgnat/s-vauspe.adb | 5 +++++ 15 files changed, 66 insertions(+) diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 2f1fbd55453..beb56bfabe1 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -90,6 +90,9 @@ is (On, "non-preelaborable call not allowed in preelaborated unit"); pragma Warnings (On, "non-static constant in preelaborated unit"); + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + ----------------------- -- Local Subprograms -- ----------------------- @@ -3653,4 +3656,5 @@ is end if; end To_Pos_Int; + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end System.Arith_Double; diff --git a/gcc/ada/libgnat/s-atopri.adb b/gcc/ada/libgnat/s-atopri.adb index 9e23fa0ac91..5fc2a123a71 100644 --- a/gcc/ada/libgnat/s-atopri.adb +++ b/gcc/ada/libgnat/s-atopri.adb @@ -59,6 +59,9 @@ package body System.Atomic_Primitives is new Atomic_Compare_Exchange (Atomic_Type); begin + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + if Expected /= Desired then if Atomic_Type'Atomic_Always_Lock_Free then return My_Atomic_Compare_Exchange (Ptr, Expected'Address, Desired); @@ -68,6 +71,8 @@ package body System.Atomic_Primitives is end if; return True; + + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end Lock_Free_Try_Write; end System.Atomic_Primitives; diff --git a/gcc/ada/libgnat/s-bitops.adb b/gcc/ada/libgnat/s-bitops.adb index 30699d73175..acddd52892c 100644 --- a/gcc/ada/libgnat/s-bitops.adb +++ b/gcc/ada/libgnat/s-bitops.adb @@ -112,6 +112,9 @@ package body System.Bit_Ops is RightB : constant Bits := To_Bits (Right); begin + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + if Llen /= Rlen then return False; @@ -134,6 +137,8 @@ package body System.Bit_Ops is end if; end; end if; + + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end Bit_Eq; ------------- diff --git a/gcc/ada/libgnat/s-carsi8.adb b/gcc/ada/libgnat/s-carsi8.adb index 807dceefc58..839f157a2ee 100644 --- a/gcc/ada/libgnat/s-carsi8.adb +++ b/gcc/ada/libgnat/s-carsi8.adb @@ -58,6 +58,9 @@ package body System.Compare_Array_Signed_8 is function To_Big_Bytes is new Ada.Unchecked_Conversion (System.Address, Big_Bytes_Ptr); + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + ---------------------- -- Compare_Array_S8 -- ---------------------- @@ -147,4 +150,5 @@ package body System.Compare_Array_Signed_8 is end if; end Compare_Array_S8_Unaligned; + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end System.Compare_Array_Signed_8; diff --git a/gcc/ada/libgnat/s-carun8.adb b/gcc/ada/libgnat/s-carun8.adb index b0f2d94bf8a..b20e4e1b922 100644 --- a/gcc/ada/libgnat/s-carun8.adb +++ b/gcc/ada/libgnat/s-carun8.adb @@ -57,6 +57,9 @@ package body System.Compare_Array_Unsigned_8 is function To_Big_Bytes is new Ada.Unchecked_Conversion (System.Address, Big_Bytes_Ptr); + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + ---------------------- -- Compare_Array_U8 -- ---------------------- @@ -146,4 +149,5 @@ package body System.Compare_Array_Unsigned_8 is end if; end Compare_Array_U8_Unaligned; + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end System.Compare_Array_Unsigned_8; diff --git a/gcc/ada/libgnat/s-casi16.adb b/gcc/ada/libgnat/s-casi16.adb index 6d35d33b9d7..fa529c9d559 100644 --- a/gcc/ada/libgnat/s-casi16.adb +++ b/gcc/ada/libgnat/s-casi16.adb @@ -58,6 +58,9 @@ package body System.Compare_Array_Signed_16 is -- Compare_Array_S16 -- ----------------------- + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + function Compare_Array_S16 (Left : System.Address; Right : System.Address; @@ -130,4 +133,5 @@ package body System.Compare_Array_Signed_16 is end if; end Compare_Array_S16; + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end System.Compare_Array_Signed_16; diff --git a/gcc/ada/libgnat/s-casi32.adb b/gcc/ada/libgnat/s-casi32.adb index 52acd30794a..7ed9ec5c519 100644 --- a/gcc/ada/libgnat/s-casi32.adb +++ b/gcc/ada/libgnat/s-casi32.adb @@ -53,6 +53,9 @@ package body System.Compare_Array_Signed_32 is -- Compare_Array_S32 -- ----------------------- + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + function Compare_Array_S32 (Left : System.Address; Right : System.Address; @@ -113,4 +116,5 @@ package body System.Compare_Array_Signed_32 is end if; end Compare_Array_S32; + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end System.Compare_Array_Signed_32; diff --git a/gcc/ada/libgnat/s-casi64.adb b/gcc/ada/libgnat/s-casi64.adb index 50b6f6d1cf9..f0211107baf 100644 --- a/gcc/ada/libgnat/s-casi64.adb +++ b/gcc/ada/libgnat/s-casi64.adb @@ -53,6 +53,9 @@ package body System.Compare_Array_Signed_64 is -- Compare_Array_S64 -- ----------------------- + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + function Compare_Array_S64 (Left : System.Address; Right : System.Address; @@ -113,4 +116,5 @@ package body System.Compare_Array_Signed_64 is end if; end Compare_Array_S64; + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end System.Compare_Array_Signed_64; diff --git a/gcc/ada/libgnat/s-caun16.adb b/gcc/ada/libgnat/s-caun16.adb index 641cf292e71..43bf35b907a 100644 --- a/gcc/ada/libgnat/s-caun16.adb +++ b/gcc/ada/libgnat/s-caun16.adb @@ -58,6 +58,9 @@ package body System.Compare_Array_Unsigned_16 is -- Compare_Array_U16 -- ----------------------- + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + function Compare_Array_U16 (Left : System.Address; Right : System.Address; @@ -130,4 +133,5 @@ package body System.Compare_Array_Unsigned_16 is end if; end Compare_Array_U16; + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end System.Compare_Array_Unsigned_16; diff --git a/gcc/ada/libgnat/s-caun32.adb b/gcc/ada/libgnat/s-caun32.adb index 2c0b7721297..0a5ca12144e 100644 --- a/gcc/ada/libgnat/s-caun32.adb +++ b/gcc/ada/libgnat/s-caun32.adb @@ -53,6 +53,9 @@ package body System.Compare_Array_Unsigned_32 is -- Compare_Array_U32 -- ----------------------- + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + function Compare_Array_U32 (Left : System.Address; Right : System.Address; @@ -113,4 +116,5 @@ package body System.Compare_Array_Unsigned_32 is end if; end Compare_Array_U32; + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end System.Compare_Array_Unsigned_32; diff --git a/gcc/ada/libgnat/s-caun64.adb b/gcc/ada/libgnat/s-caun64.adb index 8a9720ffcb6..cca2069a62b 100644 --- a/gcc/ada/libgnat/s-caun64.adb +++ b/gcc/ada/libgnat/s-caun64.adb @@ -52,6 +52,9 @@ package body System.Compare_Array_Unsigned_64 is -- Compare_Array_U64 -- ----------------------- + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + function Compare_Array_U64 (Left : System.Address; Right : System.Address; @@ -112,4 +115,5 @@ package body System.Compare_Array_Unsigned_64 is end if; end Compare_Array_U64; + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end System.Compare_Array_Unsigned_64; diff --git a/gcc/ada/libgnat/s-exponn.adb b/gcc/ada/libgnat/s-exponn.adb index d7a5342b82a..a6b87eadd15 100644 --- a/gcc/ada/libgnat/s-exponn.adb +++ b/gcc/ada/libgnat/s-exponn.adb @@ -108,6 +108,9 @@ is -- Ghost variable to hold Factor**Exp between Exp and Factor updates begin + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + -- We use the standard logarithmic approach, Exp gets shifted right -- testing successive low order bits and Factor is the value of the -- base raised to the next power of 2. @@ -173,6 +176,8 @@ is pragma Assert (Big (Result) = Big (Left) ** Right); return Result; + + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end Expon; ---------------------- diff --git a/gcc/ada/libgnat/s-expont.adb b/gcc/ada/libgnat/s-expont.adb index f6b030de50c..e8260610d58 100644 --- a/gcc/ada/libgnat/s-expont.adb +++ b/gcc/ada/libgnat/s-expont.adb @@ -108,6 +108,9 @@ is -- Ghost variable to hold Factor**Exp between Exp and Factor updates begin + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "early returns for performance"); + -- We use the standard logarithmic approach, Exp gets shifted right -- testing successive low order bits and Factor is the value of the -- base raised to the next power of 2. @@ -173,6 +176,8 @@ is pragma Assert (Big (Result) = Big (Left) ** Right); return Result; + + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end Expon; ---------------------- diff --git a/gcc/ada/libgnat/s-valspe.adb b/gcc/ada/libgnat/s-valspe.adb index 56e6ed77209..e6d9df69bb7 100644 --- a/gcc/ada/libgnat/s-valspe.adb +++ b/gcc/ada/libgnat/s-valspe.adb @@ -67,6 +67,9 @@ is function Last_Number_Ghost (Str : String) return Positive is begin + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "occurs in ghost code, not executable"); + for J in Str'Range loop if Str (J) not in '0' .. '9' | '_' then return J - 1; @@ -77,6 +80,8 @@ is end loop; return Str'Last; + + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end Last_Number_Ghost; end System.Val_Spec; diff --git a/gcc/ada/libgnat/s-vauspe.adb b/gcc/ada/libgnat/s-vauspe.adb index b2fe1870b86..c58fb218999 100644 --- a/gcc/ada/libgnat/s-vauspe.adb +++ b/gcc/ada/libgnat/s-vauspe.adb @@ -56,6 +56,9 @@ package body System.Value_U_Spec with SPARK_Mode is function Last_Hexa_Ghost (Str : String) return Positive is begin + pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns", + "occurs in ghost code, not executable"); + for J in Str'Range loop if Str (J) not in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_' then return J - 1; @@ -67,6 +70,8 @@ package body System.Value_U_Spec with SPARK_Mode is end loop; return Str'Last; + + pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns"); end Last_Hexa_Ghost; -----------------------------