diff options
| author | Yannick Moy <moy@adacore.com> | 2023-01-16 10:32:49 +0000 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-15 11:36:43 +0200 |
| commit | 75fb45f0692270efa1a89590e0d7dd0688101e8b (patch) | |
| tree | 5649e9cba2f6eaec09db48e7e28778d11a3aa6eb /libgcc | |
| parent | 2b38d009954b8e46adcb4b02a29ee631efd300ae (diff) | |
| download | gcc-75fb45f0692270efa1a89590e0d7dd0688101e8b.zip gcc-75fb45f0692270efa1a89590e0d7dd0688101e8b.tar.gz gcc-75fb45f0692270efa1a89590e0d7dd0688101e8b.tar.bz2 | |
ada: Recover proof of Interfaces.C for termination
GNATprove reports possible non-terminating loops in functions
marked as terminating. Add loop variants to prove loop termination.
gcc/ada/
* libgnat/i-c.adb: Add loop variants. Remove useless
initialization.
Diffstat (limited to 'libgcc')
0 files changed, 0 insertions, 0 deletions