[S] Change in libgfxinit[master]: gma: Work around GNATprove issue with nested loops

[Nico Huber (Code Review)]

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 
---
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