[coreboot-gerrit] [S] Change in libgfxinit[master]: framebuffer filler: Extend loop invariant to assist prover

[Nico Huber (Code Review)]

Nico Huber has uploaded this change for review. ( https://review.coreboot.org/c/libgfxinit/+/68106 )

Change subject: framebuffer filler: Extend loop invariant to assist prover
......................................................................

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 
---
M common/hw-gfx-framebuffer_filler.adb
1 file changed, 17 insertions(+), 1 deletion(-)

git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/06/68106/1

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;