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 <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/68111
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
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