framebuffer filler: Extend loop invariant to assist prover
Automatically proving that `Linux_Start + Col` is still within
`Width * Height` only worked sporadically. So we let GNATprove
show an intermediate step first to assist it.
Change-Id: I34d5b4d5840fd2b45c4bf3d72abba88487dda2dd
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/68106
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
diff --git a/common/hw-gfx-framebuffer_filler.adb b/common/hw-gfx-framebuffer_filler.adb
index 29c7da6..c6f1841 100644
--- a/common/hw-gfx-framebuffer_filler.adb
+++ b/common/hw-gfx-framebuffer_filler.adb
@@ -38,7 +38,9 @@
for Line in 0 .. Framebuffer.Height - 1 loop
pragma Loop_Invariant (Line_Start = Line * Framebuffer.Stride);
for Col in 0 .. Framebuffer.Width - 1 loop
- pragma Loop_Invariant (Line_Start = Line * Framebuffer.Stride);
+ pragma Loop_Invariant
+ (Line_Start = Line * Framebuffer.Stride and
+ Line_Start <= (Height_Type'Last - 1) * Width_Type'Last);
FB.Write (FB_Index (Line_Start + Col), 16#ff000000#);
end loop;
Line_Start := Line_Start + Framebuffer.Stride;