[Ada] Add ghost code to facilitate proof with SPARK
Proof of generic units for Long_Long_Long_Unsigned instantiations is harder for provers, as they have to deal with larger values. Add ghost code to make the proof easier. gcc/ada/ * libgnat/s-imageu.adb (Set_Image_Unsigned): Add lemma. * libgnat/s-valueu.adb (Scan_Raw_Unsigned): Add assertion.
This commit is contained in:
parent
bbb4320bae
commit
86c7b1617f
|
@ -210,6 +210,15 @@ package body System.Image_U is
|
|||
-- Ghost lemma to prove the value of a character corresponding to the
|
||||
-- next figure.
|
||||
|
||||
procedure Prove_Euclidian (Val, Quot, Rest : Uns)
|
||||
with
|
||||
Ghost,
|
||||
Pre => Quot = Val / 10
|
||||
and then Rest = Val rem 10,
|
||||
Post => Val = 10 * Quot + Rest;
|
||||
-- Ghost lemma to prove the relation between the quotient/remainder of
|
||||
-- division by 10 and the initial value.
|
||||
|
||||
procedure Prove_Hexa_To_Unsigned_Ghost (R : Uns)
|
||||
with
|
||||
Ghost,
|
||||
|
@ -256,6 +265,7 @@ package body System.Image_U is
|
|||
-----------------------------
|
||||
|
||||
procedure Prove_Character_Val (R : Uns) is null;
|
||||
procedure Prove_Euclidian (Val, Quot, Rest : Uns) is null;
|
||||
procedure Prove_Hexa_To_Unsigned_Ghost (R : Uns) is null;
|
||||
procedure Prove_Unchanged is null;
|
||||
|
||||
|
@ -347,6 +357,9 @@ package body System.Image_U is
|
|||
Acc => Value);
|
||||
|
||||
if J /= Nb_Digits then
|
||||
Prove_Euclidian (Val => Prev_Value,
|
||||
Quot => Value,
|
||||
Rest => Hexa_To_Unsigned_Ghost (S (P + J)));
|
||||
pragma Assert
|
||||
(Prev_Value = 10 * Value + Hexa_To_Unsigned_Ghost (S (P + J)));
|
||||
Prove_Iter_Scan
|
||||
|
|
|
@ -590,6 +590,10 @@ package body System.Value_U is
|
|||
if Str (P) = Base_Char then
|
||||
Ptr.all := P + 1;
|
||||
pragma Assert (Ptr.all = Last_Num_Based + 2);
|
||||
pragma Assert
|
||||
(if not Overflow then
|
||||
Based_Val = Scan_Based_Number_Ghost
|
||||
(Str, P, Last_Num_Based, Base, Uval));
|
||||
Lemma_End_Of_Scan (Str, P, Last_Num_Based, Base, Uval);
|
||||
pragma Assert (if not Overflow then Uval = Based_Val.Value);
|
||||
exit;
|
||||
|
|
Loading…
Reference in New Issue