| commit | 68d5f8bdf16ba80f0b4326a6b2da1722f95f0546 | |
| author | Yannick Moy <moy@adacore.com> | |
| Thu, 30 Mar 2023 13:07:09 +0000 (30 15:07 +0200) | ||
| committer | Marc Poulhiès <poulhies@adacore.com> | |
| Mon, 29 May 2023 08:23:18 +0000 (29 10:23 +0200) | ||
| tree | f55dc476f21e831af203233048714e556ddef85e | treesnapshot (tar.gz zip) |
| parent | 4c33d93bfe8582375d4e56faebb911854517a9f3 | commitdiff |
ada: Restore SPARK_Mode On for numerical functions
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.
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.
| gcc/ada/libgnat/a-ngelfu.ads | diffblobblamehistory |