Complete functional specification of this unit based on the Ada RM requirements in Ada RM A.3.2. This includes also obsolete subprograms moved to Ada.Characters.Conversions in Ada 2005.
GNATprove proves both absence of runtime errors and that the code
correctly implements the specified contracts.
We add a ghost type and ghost function to the public interface of
Ada.Strings.Maps to be able to express the specification of Value. In
order to minimize the risk of a naming conflict when Ada.Strings.Maps is
with'ed/use'd, we prefix the name of such ghost entities with
"SPARK_Proof".
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/a-chahan.adb: Add loop invariants as needed to prove
subprograms. Also use extended return statements where
appropriate and not done already. Mark data with
Relaxed_Initialization where needed for initialization by parts.
Convert regular functions to expression functions where needed
for proof.
* libgnat/a-chahan.ads: Add postconditions.
* libgnat/a-strmap.ads (Model): New ghost function to create a
publicly visible model of the private data Character_Mapping,
needed in order to prove subprograms in Ada.Characters.Handling.
patch.diff.gz
Description: application/gzip
