tree 3e9ec72ad288e354db74efbbf7d1efa55e865a2c
parent 17cfc92f402493979783585b6581efbd98c0cf07
author Nico Huber <nico.h@gmx.de> 1662301770 +0000
committer Nico Huber <nico.h@gmx.de> 1721232091 +0000

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>