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 /gcc/ada | |
| 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 'gcc/ada')
| -rw-r--r-- | gcc/ada/libgnat/i-c.adb | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/gcc/ada/libgnat/i-c.adb b/gcc/ada/libgnat/i-c.adb index 4cfccf4..9236189 100644 --- a/gcc/ada/libgnat/i-c.adb +++ b/gcc/ada/libgnat/i-c.adb @@ -186,7 +186,7 @@ is (Item : char_array; Trim_Nul : Boolean := True) return String is - Count : Natural := 0; + Count : Natural; From : size_t; begin @@ -200,6 +200,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -257,6 +258,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -333,6 +335,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= wide_nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -390,6 +393,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= wide_nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -466,6 +470,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= char16_nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -523,6 +528,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= char16_nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -599,6 +605,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= char32_nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; @@ -656,6 +663,7 @@ is pragma Loop_Invariant (for all J in Item'First .. From when J /= From => Item (J) /= char32_nul); + pragma Loop_Variant (Increases => From); if From > Item'Last then raise Terminator_Error; |