Attention is currently required from: Angel Pons, Nico Huber.
Hello Angel Pons,
I'd like you to reexamine a change. Please visit
https://review.coreboot.org/c/libgfxinit/+/68112?usp=email
to look at the new patch set (#2).
Change subject: gma: Work around GNATprove issue with nested loops ......................................................................
gma: Work around GNATprove issue with nested loops
Add some explicit `Loop_Invariant (True)` to work around odd check messages. These show up since about the spark- community-2019 release and still with newer versions, which almost seem to hang (takes a some minutes longer than expected). Example messages are Provided below. Given that the values are in the ranges as stated by the `for` loops, they can't be out of range.
hw-gfx-gma-plls.adb:323:14: medium: range check might fail 323 | for M1 in reverse M1_Range range Limits.M1_Lower .. Limits.M1_Upper | ^~
hw-gfx-gma-plls.adb:325:17: medium: range check might fail 325 | for M2 in reverse M2_Range range Limits.M2_Lower .. Int64'Min (Limits.M2_Upper, M1) | ^~
hw-gfx-gma-plls.adb:327:20: medium: range check might fail 327 | for P1 in reverse P1_Range range Limits.P1_Lower .. Limits.P1_Upper | ^~
hw-gfx-gma-plls.adb:332:41: medium: range check might fail 332 | M2 => M2, | ^~ reason for check: input value must fit in parameter type
Change-Id: I5430081767c760b85401300e0db4d26fd78270d7 Signed-off-by: Nico Huber nico.h@gmx.de --- M common/g45/hw-gfx-gma-plls.adb M common/ironlake/hw-gfx-gma-plls.adb 2 files changed, 4 insertions(+), 0 deletions(-)
git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/12/68112/2