https://gcc.gnu.org/g:6e0494ecf00540b996014e3bc6db6a2d6529c6d7
commit r15-256-g6e0494ecf00540b996014e3bc6db6a2d6529c6d7
Author: Joffrey Huguet <hug...@adacore.com>
Date: Mon Jan 15 17:20:47 2024 +0100
ada: Add Global contracts to Ada.Numerics.Generic_Elementary_Functions
GNATprove raised warnings about unspecified Global contracts when
using functions from an instance of
Ada.Numerics.Generic_Elementary_Functions. This patch adds null Global
contracts to all subprograms.
gcc/ada/
* libgnat/a-ngelfu.ads (Sqrt): Add Global contracts.
(Log): Likewise.
(Exp): Likewise.
("**"): Likewise.
(Sin): Likewise.
(Cos): Likewise.
(Tan): Likewise.
(Cot): Likewise.
(Arcsin): Likewise.
(Arccos): Likewise.
(Arctan): Likewise.
(Arccot): Likewise.
(Sinh): Likewise.
(Cosh): Likewise.
(Tanh): Likewise.
(Coth): Likewise.
(Arcsinh): Likewise.
(Arccosh): Likewise.
(Arctanh): Likewise.
(Arccoth): Likewise.
Diff:
---
gcc/ada/libgnat/a-ngelfu.ads | 120 ++++++++++++++++++++++++++-----------------
1 file changed, 74 insertions(+), 46 deletions(-)
diff --git a/gcc/ada/libgnat/a-ngelfu.ads b/gcc/ada/libgnat/a-ngelfu.ads
index 0dfea78aa90..774c2c6152c 100644
--- a/gcc/ada/libgnat/a-ngelfu.ads
+++ b/gcc/ada/libgnat/a-ngelfu.ads
@@ -51,8 +51,9 @@ is
pragma Assertion_Policy (Pre => Ignore);
function Sqrt (X : Float_Type'Base) return Float_Type'Base with
- Pre => X >= 0.0,
- Post => Sqrt'Result >= 0.0
+ Global => null,
+ Pre => X >= 0.0,
+ Post => Sqrt'Result >= 0.0
and then (if X = 0.0 then Sqrt'Result = 0.0)
and then (if X = 1.0 then Sqrt'Result = 1.0)
@@ -74,19 +75,23 @@ is
and then (if X >= Float_Type'Succ (0.0) then Sqrt'Result > 0.0);
function Log (X : Float_Type'Base) return Float_Type'Base with
- Pre => X > 0.0,
- Post => (if X = 1.0 then Log'Result = 0.0);
+ Global => null,
+ Pre => X > 0.0,
+ Post => (if X = 1.0 then Log'Result = 0.0);
function Log (X, Base : Float_Type'Base) return Float_Type'Base with
- Pre => X > 0.0 and Base > 0.0 and Base /= 1.0,
- Post => (if X = 1.0 then Log'Result = 0.0);
+ Global => null,
+ Pre => X > 0.0 and Base > 0.0 and Base /= 1.0,
+ Post => (if X = 1.0 then Log'Result = 0.0);
function Exp (X : Float_Type'Base) return Float_Type'Base with
- Post => (if X = 0.0 then Exp'Result = 1.0);
+ Global => null,
+ Post => (if X = 0.0 then Exp'Result = 1.0);
function "**" (Left, Right : Float_Type'Base) return Float_Type'Base with
- Pre => (if Left = 0.0 then Right > 0.0) and Left >= 0.0,
- Post => "**"'Result >= 0.0
+ Global => null,
+ Pre => (if Left = 0.0 then Right > 0.0) and Left >= 0.0,
+ Post => "**"'Result >= 0.0
and then (if Right = 0.0 then "**"'Result = 1.0)
and then (if Right = 1.0 then "**"'Result = Left)
and then (if Left = 1.0 then "**"'Result = 1.0)
@@ -94,115 +99,138 @@ is
function Sin (X : Float_Type'Base) return Float_Type'Base with
Inline,
- Post => Sin'Result in -1.0 .. 1.0
+ Global => null,
+ Post => Sin'Result in -1.0 .. 1.0
and then (if X = 0.0 then Sin'Result = 0.0);
function Sin (X, Cycle : Float_Type'Base) return Float_Type'Base with
- Pre => Cycle > 0.0,
- Post => Sin'Result in -1.0 .. 1.0
+ Global => null,
+ Pre => Cycle > 0.0,
+ Post => Sin'Result in -1.0 .. 1.0
and then (if X = 0.0 then Sin'Result = 0.0);
function Cos (X : Float_Type'Base) return Float_Type'Base with
Inline,
- Post => Cos'Result in -1.0 .. 1.0
+ Global => null,
+ Post => Cos'Result in -1.0 .. 1.0
and then (if X = 0.0 then Cos'Result = 1.0);
function Cos (X, Cycle : Float_Type'Base) return Float_Type'Base with
- Pre => Cycle > 0.0,
- Post => Cos'Result in -1.0 .. 1.0
+ Global => null,
+ Pre => Cycle > 0.0,
+ Post => Cos'Result in -1.0 .. 1.0
and then (if X = 0.0 then Cos'Result = 1.0);
function Tan (X : Float_Type'Base) return Float_Type'Base with
- Post => (if X = 0.0 then Tan'Result = 0.0);
+ Global => null,
+ Post => (if X = 0.0 then Tan'Result = 0.0);
function Tan (X, Cycle : Float_Type'Base) return Float_Type'Base with
- Pre => Cycle > 0.0
+ Global => null,
+ Pre => Cycle > 0.0
and then abs Float_Type'Base'Remainder (X, Cycle) /= 0.25 * Cycle,
- Post => (if X = 0.0 then Tan'Result = 0.0);
+ Post => (if X = 0.0 then Tan'Result = 0.0);
function Cot (X : Float_Type'Base) return Float_Type'Base with
- Pre => X /= 0.0;
+ Global => null,
+ Pre => X /= 0.0;
function Cot (X, Cycle : Float_Type'Base) return Float_Type'Base with
- Pre => Cycle > 0.0
+ Global => null,
+ 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;
function Arcsin (X : Float_Type'Base) return Float_Type'Base with
- Pre => abs X <= 1.0,
- Post => (if X = 0.0 then Arcsin'Result = 0.0);
+ Global => null,
+ Pre => abs X <= 1.0,
+ Post => (if X = 0.0 then Arcsin'Result = 0.0);
function Arcsin (X, Cycle : Float_Type'Base) return Float_Type'Base with
- Pre => Cycle > 0.0 and abs X <= 1.0,
- Post => (if X = 0.0 then Arcsin'Result = 0.0);
+ Global => null,
+ Pre => Cycle > 0.0 and abs X <= 1.0,
+ Post => (if X = 0.0 then Arcsin'Result = 0.0);
function Arccos (X : Float_Type'Base) return Float_Type'Base with
- Pre => abs X <= 1.0,
- Post => (if X = 1.0 then Arccos'Result = 0.0);
+ Global => null,
+ Pre => abs X <= 1.0,
+ Post => (if X = 1.0 then Arccos'Result = 0.0);
function Arccos (X, Cycle : Float_Type'Base) return Float_Type'Base with
- Pre => Cycle > 0.0 and abs X <= 1.0,
- Post => (if X = 1.0 then Arccos'Result = 0.0);
+ Global => null,
+ Pre => Cycle > 0.0 and abs X <= 1.0,
+ Post => (if X = 1.0 then Arccos'Result = 0.0);
function Arctan
(Y : Float_Type'Base;
X : Float_Type'Base := 1.0) return Float_Type'Base
with
- Pre => X /= 0.0 or Y /= 0.0,
- Post => (if X > 0.0 and then Y = 0.0 then Arctan'Result = 0.0);
+ Global => null,
+ Pre => X /= 0.0 or Y /= 0.0,
+ Post => (if X > 0.0 and then Y = 0.0 then Arctan'Result = 0.0);
function Arctan
(Y : Float_Type'Base;
X : Float_Type'Base := 1.0;
Cycle : Float_Type'Base) return Float_Type'Base
with
- Pre => Cycle > 0.0 and (X /= 0.0 or Y /= 0.0),
- Post => (if X > 0.0 and then Y = 0.0 then Arctan'Result = 0.0);
+ Global => null,
+ Pre => Cycle > 0.0 and (X /= 0.0 or Y /= 0.0),
+ Post => (if X > 0.0 and then Y = 0.0 then Arctan'Result = 0.0);
function Arccot
(X : Float_Type'Base;
Y : Float_Type'Base := 1.0) return Float_Type'Base
with
- Pre => X /= 0.0 or Y /= 0.0,
- Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0);
+ Global => null,
+ Pre => X /= 0.0 or Y /= 0.0,
+ Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0);
function Arccot
(X : Float_Type'Base;
Y : Float_Type'Base := 1.0;
Cycle : Float_Type'Base) return Float_Type'Base
with
- Pre => Cycle > 0.0 and (X /= 0.0 or Y /= 0.0),
- Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0);
+ Global => null,
+ Pre => Cycle > 0.0 and (X /= 0.0 or Y /= 0.0),
+ Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0);
function Sinh (X : Float_Type'Base) return Float_Type'Base with
Post => (if X = 0.0 then Sinh'Result = 0.0);
function Cosh (X : Float_Type'Base) return Float_Type'Base with
- Post => Cosh'Result >= 1.0
+ Global => null,
+ Post => Cosh'Result >= 1.0
and then (if X = 0.0 then Cosh'Result = 1.0);
function Tanh (X : Float_Type'Base) return Float_Type'Base with
- Post => Tanh'Result in -1.0 .. 1.0
+ Global => null,
+ Post => Tanh'Result in -1.0 .. 1.0
and then (if X = 0.0 then Tanh'Result = 0.0);
function Coth (X : Float_Type'Base) return Float_Type'Base with
- Pre => X /= 0.0,
- Post => abs Coth'Result >= 1.0;
+ Global => null,
+ Pre => X /= 0.0,
+ Post => abs Coth'Result >= 1.0;
function Arcsinh (X : Float_Type'Base) return Float_Type'Base with
- Post => (if X = 0.0 then Arcsinh'Result = 0.0);
+ Global => null,
+ Post => (if X = 0.0 then Arcsinh'Result = 0.0);
function Arccosh (X : Float_Type'Base) return Float_Type'Base with
- Pre => X >= 1.0,
- Post => Arccosh'Result >= 0.0
+ Global => null,
+ Pre => X >= 1.0,
+ Post => Arccosh'Result >= 0.0
and then (if X = 1.0 then Arccosh'Result = 0.0);
function Arctanh (X : Float_Type'Base) return Float_Type'Base with
- Pre => abs X < 1.0,
- Post => (if X = 0.0 then Arctanh'Result = 0.0);
+ Global => null,
+ Pre => abs X < 1.0,
+ Post => (if X = 0.0 then Arctanh'Result = 0.0);
function Arccoth (X : Float_Type'Base) return Float_Type'Base with
- Pre => abs X > 1.0;
+ Global => null,
+ Pre => abs X > 1.0;
end Ada.Numerics.Generic_Elementary_Functions;
