diff options
| author | Claire Dross <dross@adacore.com> | 2023-03-30 11:09:33 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-06-20 09:30:48 +0200 |
| commit | b1c3d01619e06e7ef49097925b81307f422ec78a (patch) | |
| tree | 1ce59b29c1ea20b38af2922a1438ac976b7834da /gcc/ada/libgnat/interfac.ads | |
| parent | 862f84b4a36d6c569968d20949f54e2f427179c1 (diff) | |
| download | gcc-b1c3d01619e06e7ef49097925b81307f422ec78a.zip gcc-b1c3d01619e06e7ef49097925b81307f422ec78a.tar.gz gcc-b1c3d01619e06e7ef49097925b81307f422ec78a.tar.bz2 | |
ada: Remove references to Might_Not_Return and Always_Return
The Might_Not_Return and Always_Return annotations for GNATprove
should now be replaced by the two more precise aspects
Exceptional_Cases and Always_Terminates.
They allow to specify whether a subprogram is allowed to raise
exceptions or fail to complete.
gcc/ada/
* libgnat/a-strfix.ads: Replace Might_Not_Return annotations by
Exceptional_Cases and Always_Terminates aspects.
* libgnat/a-tideio.ads: Idem.
* libgnat/a-tienio.ads: Idem.
* libgnat/a-tifiio.ads: Idem.
* libgnat/a-tiflio.ads: Idem.
* libgnat/a-tiinio.ads: Idem.
* libgnat/a-timoio.ads: Idem.
* libgnat/a-textio.ads: Idem. Also mark functions Name, Col, Line,
and Page as out of SPARK as they might raise Layout_Error.
* libgnarl/a-reatim.ads: Replace Always_Return annotations by
Always_Terminates aspects.
* libgnat/a-chahan.ads: Idem.
* libgnat/a-nbnbig.ads: Idem.
* libgnat/a-nbnbin.ads: Idem.
* libgnat/a-nbnbre.ads: Idem.
* libgnat/a-ngelfu.ads: Idem.
* libgnat/a-nlelfu.ads: Idem.
* libgnat/a-nllefu.ads: Idem.
* libgnat/a-nselfu.ads: Idem.
* libgnat/a-nuelfu.ads: Idem.
* libgnat/a-strbou.ads: Idem.
* libgnat/a-strmap.ads: Idem.
* libgnat/a-strsea.ads: Idem.
* libgnat/a-strsup.ads: Idem.
* libgnat/a-strunb.ads: Idem.
* libgnat/a-strunb__shared.ads: Idem.
* libgnat/g-souinf.ads: Idem.
* libgnat/i-c.ads: Idem.
* libgnat/interfac.ads: Idem.
* libgnat/interfac__2020.ads: Idem.
* libgnat/s-aridou.adb: Idem.
* libgnat/s-arit32.adb: Idem.
* libgnat/s-atacco.ads: Idem.
* libgnat/s-spcuop.ads: Idem.
* libgnat/s-stoele.ads: Idem.
* libgnat/s-vaispe.ads: Idem.
* libgnat/s-vauspe.ads: Idem.
* libgnat/i-cstrin.ads: Add a precondition instead of a
Might_Not_Return annotation.
Diffstat (limited to 'gcc/ada/libgnat/interfac.ads')
| -rw-r--r-- | gcc/ada/libgnat/interfac.ads | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/gcc/ada/libgnat/interfac.ads b/gcc/ada/libgnat/interfac.ads index edd3f36..bc37a8e 100644 --- a/gcc/ada/libgnat/interfac.ads +++ b/gcc/ada/libgnat/interfac.ads @@ -35,10 +35,11 @@ -- This is the compiler version of this unit -package Interfaces is +package Interfaces with + Always_Terminates +is pragma No_Elaboration_Code_All; pragma Pure; - pragma Annotate (GNATprove, Always_Return, Interfaces); -- All identifiers in this unit are implementation defined |