[Ada] Proof of Ada.Characters.Handling

[Ada] Proof of Ada.Characters.Handling

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 1200 bytes --]

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.

[-- Attachment #2: patch.diff.gz --]
[-- Type: application/gzip, Size: 5359 bytes --]