From: Yannick Moy <moy@adacore.com>
Date: Mon, 17 May 2021 13:58:26 +0000 (+0200)
Subject: [Ada] Fix precondition of Cot for code analyzers
X-Git-Tag: basepoints/gcc-13~6205
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=d557a5f9cea39c4871af06e0684f94590d8bd97d;p=thirdparty%2Fgcc.git

[Ada] Fix precondition of Cot for code analyzers

gcc/ada/

	* libgnat/a-ngelfu.ads (Cot): Fix precondition.
---

diff --git a/gcc/ada/libgnat/a-ngelfu.ads b/gcc/ada/libgnat/a-ngelfu.ads
index 055c2823450b..523e64ff9710 100644
--- a/gcc/ada/libgnat/a-ngelfu.ads
+++ b/gcc/ada/libgnat/a-ngelfu.ads
@@ -126,7 +126,7 @@ is
      Pre => Cycle > 0.0
        and then X /= 0.0
        and then Float_Type'Base'Remainder (X, Cycle) /= 0.0
-       and then abs Float_Type'Base'Remainder (X, Cycle) = 0.5 * Cycle;
+       and then abs Float_Type'Base'Remainder (X, Cycle) /= 0.5 * Cycle;
 
    function Arcsin (X : Float_Type'Base) return Float_Type'Base with
      Pre  => abs X <= 1.0,