Introduced pragmas to prove with SPARK the behaviours of most of the functions and procedures from Ada.Strings.Fixed. Procedure Move and all procedures that rely on it (Insert, Delete, Overwrite, Replace_Slice) have incomplete contracts and can have runtime errors. Function Count is given without a postcondition because it would be hard to express, but absence of runtime errors is ensured. The private package Ada.Strings.Search has also been made public, to allow the use of Match in the contracts of Ada.Strings.Fixed.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/a-strfix.adb ("*"): Added loop invariants and lemmas
for proof.
(Delete): Added assertions for proof, and conditions to avoid
overflow.
(Head): Added loop invariant.
(Insert): Same as Delete.
(Move): Declared with SPARK_Mode Off.
(Overwrite): Added assertions for proof, and conditions to avoid
overflow.
(Replace_Slice): Added assertions for proof, and conditions to
avoid overflow.
(Tail): Added loop invariant and avoided overflows.
(Translate): Added loop invariants.
(Trim): Ensured empty strings returned start at 1.
* libgnat/a-strfix.ads (Index): Rewrote contract cases for
easier proof.
(Index_Non_Blank): Separated the null string case.
(Count): Specified Mapping shouldn't be null.
(Find_Token): Specified Source'First should be Positive when no
From is given.
(Translate): Specified Mapping shouldn't be null.
("*"): Rewrote postcondition for easier proof.
* libgnat/a-strsea.adb (Belongs): Added postcondition.
(Count): Rewrote loops and added loop invariants to avoid
overflows.
(Find_Token): Added loop invariants.
(Index): Rewrote loops to avoid overflows and added loop
invariants for proof.
(Index_Non_Blank): Added loop invariants.
(Is_Identity): New function isolated without SPARK_Mode.
* libgnat/a-strsea.ads: Fix starting comment as package is no
longer private.
(Match): Declared ghost expression function Match.
(Is_Identity): Described identity in the postcondition.
(Index, Index_Non_Blank, Count, Find_Token): Added contract from
a-strfix.ads.
patch.diff.gz
Description: application/gzip
