tree 68ff79eedee669448375748c4a914ec841f97c77
parent 420e863442eb72c35fa3b8a32313980853ba4cff
author Nico Huber <nico.h@gmx.de> 1662289706 +0200
committer Nico Huber <nico.h@gmx.de> 1669654815 +0000

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>