OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Recover proof of Ada.Strings.Fixed with assertions

Browse Source 
gcc/ada/

	* libgnat/a-strfix.adb (Insert, Overwrite): Add assertions.
This commit is contained in:
Yannick Moy 2022-01-05 10:43:25 +01:00 committed by Pierre-Marie de Rodat
parent 7aa3800216
commit 87f152ba31
1 changed files with 13 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
gcc/ada/libgnat/a-strfix.adb
View File

@ -384,6 +384,10 @@ package body Ada.Strings.Fixed with SPARK_Mode is
Source (Source'First .. Before - 1);
Result (Front + 1 .. Front + New_Item'Length) :=
New_Item;
pragma Assert
(Result (1 .. Before - Source'First)
= Source (Source'First .. Before - 1));
pragma Assert
(Result
(Before - Source'First + 1
@ -558,15 +562,21 @@ package body Ada.Strings.Fixed with SPARK_Mode is
if Position <= Source'Last - New_Item'Length then
Result (Front + New_Item'Length + 1 .. Result'Last) :=
Source (Position + New_Item'Length .. Source'Last);
pragma Assert
(Result
(Position - Source'First + New_Item'Length + 1
.. Result'Last)
= Source (Position + New_Item'Length .. Source'Last));
end if;
pragma Assert
(if Position <= Source'Last - New_Item'Length
then
Result
(Position - Source'First + New_Item'Length + 1
.. Result'Last)
= Source (Position + New_Item'Length .. Source'Last));
(Position - Source'First + New_Item'Length + 1
.. Result'Last)
= Source (Position + New_Item'Length .. Source'Last));
end return;
end;
end Overwrite;