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 (#3).
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 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/3