diff mbox series

[COMMITTED] ada: Add Global contracts to Ada.Numerics.Generic_Elementary_Functions

Message ID 20240507080025.37617-1-poulhies@adacore.com
State Committed
Headers
Series [COMMITTED] ada: Add Global contracts to Ada.Numerics.Generic_Elementary_Functions |

Checks

Context Check Description
linaro-tcwg-bot/tcwg_gcc_build--master-arm warning Patch is already merged
linaro-tcwg-bot/tcwg_gcc_build--master-aarch64 warning Patch is already merged

Commit Message

Marc Poulhiès May 7, 2024, 8 a.m. UTC 
  From: Joffrey Huguet <huguet@adacore.com>

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.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/a-ngelfu.ads | 120 +++++++++++++++++++++--------------
 1 file changed, 74 insertions(+), 46 deletions(-)
diff mbox series

Patch

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;