Nico Huber has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35750 )
Change subject: Increase range of our main Frequency_Type ......................................................................
Patch Set 2:
(1 comment)
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... File common/hw-gfx-gma-pch-vga.adb:
https://review.coreboot.org/c/libgfxinit/+/35750/2/common/hw-gfx-gma-pch-vga... PS2, Line 138: Div_Sel := Word32 (Refclock / Mode.Dotclock) - 2;
I would prefer if this were to be proven rather than relying on overflow handling behavior
What we rely on is not the behaviour of the numbers here but that this code is never called to enable a VGA port with an order-of-magnitude too high frequency. Which we know that we don't do.
But if you want to prove it, be my guest :)
What makes it difficult to get it proved with GNATprove is also the assumption that this code is only called for FDI connections (which will always be the case). So we'd need the precondition here that `Dotclock < 1_350_000_000`. A level up add `Display = VGA and` and another level up add `Gen = Haswell and` because then we know that VGA is al- ways used with FDI. And finally, in Fill_Port_Config() prove that `Display = VGA and Gen = Haswell => FDI` and that FDI config only succeeds if `Dotclock < X` (X is depends on the BPC also). That prove might need some refactoring so that would result in another (small) patch train... As all that wouldn't change the program behaviour, it's really just an academic excercise. Sure, we could prove correct behaviour of this program, but so far proving absence of runtime errors alone adds enough burden oO