[S] Change in libgfxinit[master]: gma: Correct Global annotation for Initialize()

[Nico Huber (Code Review)]

Nico Huber has uploaded this change for review. ( https://review.coreboot.org/c/libgfxinit/+/68111 )

Change subject: gma: Correct Global annotation for Initialize()
......................................................................

gma: Correct Global annotation for Initialize()

On G45, we use the private PCI device `Dev` during
Power_And_Clocks.Initialize(). As its `Dev.PCI_State`
is not directly visible in the sub-package, it is
assumed that the whole, abstract `Device_State` can
be altered. This includes `Registers.GTT_State`.

Correcting the `Globals` aspect for G45 makes it
excessive for other platforms, hence we need the
same forest of additional justifications and anno-
tations as we have for Power_Up_VGA().

Change-Id: I7086b024d96f0a17f19f46f60ceac6757eb91867
Signed-off-by: Nico Huber 
---
M common/hw-gfx-gma.adb
1 file changed, 35 insertions(+), 1 deletion(-)

git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/11/68111/1

diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index 87c8fb0..1db493f 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -436,6 +436,11 @@

----------------------------------------------------------------------------

+   pragma Warnings
+     (GNATprove, Off, """Registers.GTT_State"" * is not modified*",
+      Reason => "The whole, abstract Device_State is modified in certain configurations.");
+   pragma Warnings
+     (GNATprove, Off, "no check message justified*", Reason => "see below");
    procedure Initialize
      (Write_Delay : in     Word64 := 0;
       Clean_State : in     Boolean := False;
@@ -443,7 +448,9 @@
    with
       Refined_Global =>
         (Input => (Time.State),
-         In_Out => (Dev.PCI_State, Registers.Register_State, Port_IO.State),
+         In_Out =>
+           (Dev.PCI_State, Port_IO.State,
+            Registers.Register_State, Registers.GTT_State),
          Output =>
            (PCI_Usable,
             Config.Variable,
@@ -592,6 +599,12 @@
       Initialized := True;

end Initialize;
+   pragma Annotate
+     (GNATprove, Intentional, "unused global",
+      "The whole, abstract Device_State is modified in certain configurations.");
+   pragma Warnings (GNATprove, On, "no check message justified*");
+   pragma Warnings
+     (GNATprove, On, """Registers.GTT_State"" * is not modified*");

function Is_Initialized return Boolean
    with