OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Fix proof of runtime unit s-valeu

Browse Source 
Update to provers caused some proof regressions.  Fix the proof by
changing ghost code.

gcc/ada/

	* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Add assertions.
This commit is contained in:
Claire Dross 2022-04-08 16:38:47 +02:00 committed by Pierre-Marie de Rodat
parent df4451ca66
commit 6f8f9d1bcf
1 changed files with 8 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
gcc/ada/libgnat/s-valueu.adb
View File

@ -522,6 +522,9 @@ package body System.Value_U is
Uval := Base;
Base := 10;
pragma Assert (Ptr.all = Last_Num_Init + 1);
pragma Assert
(if Starts_As_Based then P = Last_Num_Based + 1);
pragma Assert (not Is_Based);
pragma Assert (if not Overflow then Uval = Init_Val.Value);
exit;
end if;
@ -569,10 +572,6 @@ package body System.Value_U is
end if;
end if;
Lemma_Scan_Digit
(Str, P, Last_Num_Based, Digit, Base, Old_Uval, Uval,
Based_Val, Old_Overflow, Overflow);
-- If at end of string with no base char, not a based number
-- but we signal Constraint_Error and set the pointer past
-- the end of the field, since this is what the ACVC tests
@ -580,6 +579,10 @@ package body System.Value_U is
P := P + 1;
Lemma_Scan_Digit
(Str, P - 1, Last_Num_Based, Digit, Base, Old_Uval, Uval,
Based_Val, Old_Overflow, Overflow);
if P > Max then
Ptr.all := P;
Bad_Value (Str);
@ -590,6 +593,7 @@ 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 (Is_Based);
pragma Assert
(if not Overflow then
Based_Val = Scan_Based_Number_Ghost