diff options
| author | Yannick Moy <moy@adacore.com> | 2023-01-16 11:33:03 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-15 11:36:43 +0200 |
| commit | 9c213cb8671e01578a3714ac136760f9452642aa (patch) | |
| tree | f0b5cd35c94f9e15e48838d1259265fd713cd790 /gcc/fortran/interface.cc | |
| parent | a398b5479c9c928f7d9999de8b0c6580b733e6a8 (diff) | |
| download | gcc-9c213cb8671e01578a3714ac136760f9452642aa.zip gcc-9c213cb8671e01578a3714ac136760f9452642aa.tar.gz gcc-9c213cb8671e01578a3714ac136760f9452642aa.tar.bz2 | |
ada: Add annotations for proof of termination of runtime units
String-manipulating functions should always terminate. Add justification
for the termination of Mapping function parameter, and loop variants
where needed. This is needed for GNATprove to prove termination.
gcc/ada/
* libgnat/a-strbou.ads: Add justifications for Mapping.
* libgnat/a-strfix.adb: Same.
* libgnat/a-strfix.ads: Same.
* libgnat/a-strsea.adb: Same.
* libgnat/a-strsea.ads: Same.
* libgnat/a-strsup.adb: Same and add loop variants.
* libgnat/a-strsup.ads: Same and add specification of termination.
Diffstat (limited to 'gcc/fortran/interface.cc')
0 files changed, 0 insertions, 0 deletions