Nico Huber has submitted this change. ( https://review.coreboot.org/c/libgfxinit/+/68112?usp=email )
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 Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/68112 Reviewed-by: Angel Pons th3fanbus@gmail.com --- M common/g45/hw-gfx-gma-plls.adb M common/ironlake/hw-gfx-gma-plls.adb 2 files changed, 4 insertions(+), 0 deletions(-)
Approvals: Nico Huber: Verified Angel Pons: Looks good to me, approved
diff --git a/common/g45/hw-gfx-gma-plls.adb b/common/g45/hw-gfx-gma-plls.adb index 67242f2..5db76d6 100644 --- a/common/g45/hw-gfx-gma-plls.adb +++ b/common/g45/hw-gfx-gma-plls.adb @@ -322,8 +322,10 @@ -- reverse loops as hardware prefers higher values for M1 in reverse M1_Range range Limits.M1_Lower .. Limits.M1_Upper loop + pragma Loop_Invariant (True); for M2 in reverse M2_Range range Limits.M2_Lower .. Int64'Min (Limits.M2_Upper, M1) loop + pragma Loop_Invariant (True); for P1 in reverse P1_Range range Limits.P1_Lower .. Limits.P1_Upper loop Verify_Parameters diff --git a/common/ironlake/hw-gfx-gma-plls.adb b/common/ironlake/hw-gfx-gma-plls.adb index 10e9ff2..8b6ca36 100644 --- a/common/ironlake/hw-gfx-gma-plls.adb +++ b/common/ironlake/hw-gfx-gma-plls.adb @@ -291,8 +291,10 @@ -- reverse loops as hardware prefers higher values for M1 in reverse M1_Range range Limits.M1_Lower .. Limits.M1_Upper loop + pragma Loop_Invariant (True); for M2 in reverse M2_Range range Limits.M2_Lower .. Limits.M2_Upper loop + pragma Loop_Invariant (True); for P1 in reverse P1_Range range Limits.P1_Lower .. Limits.P1_Upper loop Verify_Parameters