diff mbox series

[COMMITTED] ada: Restore SPARK_Mode On for numerical functions

Message ID 20230529082853.2409094-1-poulhies@adacore.com
State Committed
Commit 68d5f8bdf16ba80f0b4326a6b2da1722f95f0546
Headers
Series [COMMITTED] ada: Restore SPARK_Mode On for numerical functions |

Commit Message

Marc Poulhiès May 29, 2023, 8:28 a.m. UTC 
  From: Yannick Moy <moy@adacore.com>

GNATprove has ad-hoc support for the standard numerical functions, which
consists in emitting an unprovable preconditions on cases which could
lead to an overflow. These functions are thus valid to call from SPARK
code.

gcc/ada/

	* libgnat/a-ngelfu.ads: Restore SPARK_Mode from context.

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

---
 gcc/ada/libgnat/a-ngelfu.ads | 6 ------
 1 file changed, 6 deletions(-)
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/a-ngelfu.ads b/gcc/ada/libgnat/a-ngelfu.ads
index ae06ea710eb..f6d6c9643af 100644
--- a/gcc/ada/libgnat/a-ngelfu.ads
+++ b/gcc/ada/libgnat/a-ngelfu.ads
@@ -116,17 +116,14 @@  is
      Post => (if X = 0.0 then Tan'Result = 0.0);
 
    function Tan (X, Cycle : Float_Type'Base) return Float_Type'Base with
-     SPARK_Mode => Off,  --  Tan can overflow for some values of X and Cycle
      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);
 
    function Cot (X : Float_Type'Base) return Float_Type'Base with
-     SPARK_Mode => Off,  --  Cot can overflow for some values of X
      Pre => X /= 0.0;
 
    function Cot (X, Cycle : Float_Type'Base) return Float_Type'Base with
-     SPARK_Mode => Off,  --  Cot can overflow for some values of X and Cycle
      Pre => Cycle > 0.0
        and then X /= 0.0
        and then Float_Type'Base'Remainder (X, Cycle) /= 0.0
@@ -179,11 +176,9 @@  is
      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
-     SPARK_Mode => Off,  --  Sinh can overflow for some values of X
      Post => (if X = 0.0 then Sinh'Result = 0.0);
 
    function Cosh (X : Float_Type'Base) return Float_Type'Base with
-     SPARK_Mode => Off,  --  Cosh can overflow for some values of X
      Post => Cosh'Result >= 1.0
        and then (if X = 0.0 then Cosh'Result = 1.0);
 
@@ -192,7 +187,6 @@  is
        and then (if X = 0.0 then Tanh'Result = 0.0);
 
    function Coth (X : Float_Type'Base) return Float_Type'Base with
-     SPARK_Mode => Off,  --  Coth can overflow for some values of X
      Pre  => X /= 0.0,
      Post => abs Coth'Result >= 1.0;