diff options
| author | Yannick Moy <moy@adacore.com> | 2021-09-02 23:29:38 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-10-05 08:20:00 +0000 |
| commit | f46939f9d4091e78e60d8d4d78d023a48a1608aa (patch) | |
| tree | 4ab552062771cc195fa37fd26bddb90b9f1cf18d /gcc/ada/debug.adb | |
| parent | ec8ccc712cc15124090dab1ae44dccee280ce4ad (diff) | |
| download | gcc-f46939f9d4091e78e60d8d4d78d023a48a1608aa.zip gcc-f46939f9d4091e78e60d8d4d78d023a48a1608aa.tar.gz gcc-f46939f9d4091e78e60d8d4d78d023a48a1608aa.tar.bz2 | |
[Ada] Proof of Ada.Strings.Maps
gcc/ada/
* libgnat/a-strmap.adb: Add ghost code for proof.
(To_Range): This is the most involved proof, as it requires
creating the result of the call to To_Domain as a ghost
variable, and show the unicity of this result in order to prove
the postcondition.
* libgnat/a-strmap.ads: (SPARK_Proof_Sorted_Character_Sequence):
New ghost function.
(To_Domain): Add postcondition regarding sorting of result.
(To_Range): Fix postcondition that should compare Length instead
of Last for the results of To_Domain and To_Range, as the value
of Last for an empty result is not specified in the Ada RM.
Diffstat (limited to 'gcc/ada/debug.adb')
0 files changed, 0 insertions, 0 deletions