1 comment:
File common/hw-gfx-gma-pch-vga.adb:
Patch Set #2, 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
To view, visit change 35750. To unsubscribe, or for help writing mail filters, visit settings.