Nico Huber has posted comments on this change. ( https://review.coreboot.org/c/libhwbase/+/37530 )
Change subject: [WIP] Printf like debugging ......................................................................
Patch Set 1:
(3 comments)
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb File debug/hw-print.adb:
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@48 PS1, Line 48: Format_String'First <= Format_String'Last and First precondition seems not needed (anymore)?
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@108 PS1, Line 108: Arg.Padding := Arg.Padding * 10 + Char_To_UInt (Format_String (Pos)); GNATprove is right to complain here about potential overflows. We don't know what string we will be called with, e.g. if it starts with "%111111111111" it would overflow.
So we need to explicitly check
if Arg.Padding <= Natural'Last / 10 - 9 then
I would say, we can just ignore errors.
To prove this, we need to know that Char_To_UInt() returns at most 9. Three ways come to mind:
Make it an expression function (this way callers know exactly what it does):
function Char_To_UInt (Item : in Character) return Natural is (Character'Pos (Item) - Character'Pos ('0')) with Pre => Item in '0' .. '9';
Constrain the return type, e.g.
subtype Decimal_Digit is Natural range 0 .. 9;
Or add a post condition:
Post => Char_To_UInt'Result in 0 .. 9;
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@207 PS1, Line 207: pragma loop_invariant (Item_C < Item_B ** String_Begin);
Maybe we have to make it explicit that `Item_B` doesn't change in […]
Meh, whatever, even with that and without overflowing Word64 in the exponentiation, I don't get anything useful.
Making the code more explicit shouldn't hurt:
for Pos in reverse Word64_String_Range loop Output_String (Pos) := ... ... String_Begin := Pos; exit when Item_C = 0; end loop;