diff options
| author | Yannick Moy <moy@adacore.com> | 2023-03-30 15:07:09 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-29 10:23:18 +0200 |
| commit | 68d5f8bdf16ba80f0b4326a6b2da1722f95f0546 (patch) | |
| tree | f55dc476f21e831af203233048714e556ddef85e /gcc/ada/contracts.adb | |
| parent | 4c33d93bfe8582375d4e56faebb911854517a9f3 (diff) | |
| download | gcc-68d5f8bdf16ba80f0b4326a6b2da1722f95f0546.zip gcc-68d5f8bdf16ba80f0b4326a6b2da1722f95f0546.tar.gz gcc-68d5f8bdf16ba80f0b4326a6b2da1722f95f0546.tar.bz2 | |
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.
Diffstat (limited to 'gcc/ada/contracts.adb')
0 files changed, 0 insertions, 0 deletions