projects / platform / upstream / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 37a3df0) | patch
[Ada] Minimize parts of Ada.Strings.Fixed marked SPARK_Mode => Off
authorYannick Moy <moy@adacore.com>
Mon, 26 Jul 2021 10:21:02 +0000 (12:21 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Thu, 23 Sep 2021 13:06:13 +0000 (13:06 +0000)
commit7165704bfaae012cb28e5411619218da6fb8320d
treecf9e816b9963c52316527c21c9c2a589a8be34e9tree | snapshot
parent37a3df0d9a849c912735124ec0b156c229fb308acommit | diff
[Ada] Minimize parts of Ada.Strings.Fixed marked SPARK_Mode => Off

gcc/ada/

* libgnat/a-strfix.adb (Delete, Insert, Overwrite,
Replace_Slice): Remove SPARK_Mode Off.
* libgnat/a-strfix.ads (Insert, Overwrite, Replace_Slice):
Strengthen precondition.
gcc/ada/libgnat/a-strfix.adb diff | blob | history
gcc/ada/libgnat/a-strfix.ads diff | blob | history
Domain: System / Toolchain;