Nico Huber has uploaded this change for review. ( https://review.coreboot.org/c/libgfxinit/+/68112 )
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 weird check messages.
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, 17 insertions(+), 0 deletions(-)
git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/12/68112/1
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