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