commit 75a707f3ef80fb150fc0c3fdb69d7cb7c21480f6
author Nico Huber <nico.h@gmx.de> Mon Jun 18 16:28:33 2018 +0200
committer Nico Huber <nico.h@gmx.de> Mon Sep 02 10:09:31 2019 +0000
tree a7c6acef5bd209e8d94f43905df7ecb167ccca48
parent d8282b6330f053d298c6aec660ed95018dbfe31c

gma pipe setup: Fix secondary pipe cursors <= Sandy Bridge

The secondary cursor registers used to have a different offset.

Change-Id: I4d79f59a8cb693d73d6da666525f091021efb4fd
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/27154
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
Reviewed-by: Reto Buerki <reet@codelabs.ch>

common/hw-gfx-gma.ads

diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 8b1c85a..f9444e8 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -129,12 +129,19 @@
          Proof_In => (Init_State)),
       Pre => Is_Initialized;
 
+   pragma Warnings (GNATprove, Off, "no check message justified by this",
+                    Reason => "see Annotate aspects.");
    procedure Update_Cursor (Pipe : Pipe_Index; Cursor : Cursor_Type)
    with
       Global =>
-        (In_Out => (State, Device_State),
+        (Input => (Config_State),
+         In_Out => (State, Device_State),
          Proof_In => (Init_State)),
-      Pre => Is_Initialized;
+      Pre => Is_Initialized,
+      Annotate =>
+        (GNATprove, Intentional,
+         "global input ""GMA.Config_State"" of ""Update_Cursor"" not read",
+         "Reading of Config_State depends on the platform configuration.");
 
    procedure Place_Cursor
      (Pipe : Pipe_Index;
@@ -142,9 +149,14 @@
       Y : Cursor_Pos)
    with
       Global =>
-        (In_Out => (State, Device_State),
+        (Input => (Config_State),
+         In_Out => (State, Device_State),
          Proof_In => (Init_State)),
-      Pre => Is_Initialized;
+      Pre => Is_Initialized,
+      Annotate =>
+        (GNATprove, Intentional,
+         "global input ""GMA.Config_State"" of ""Place_Cursor"" not read",
+         "Reading of Config_State depends on the platform configuration.");
 
    procedure Move_Cursor
      (Pipe : Pipe_Index;
@@ -152,9 +164,14 @@
       Y : Cursor_Pos)
    with
       Global =>
-        (In_Out => (State, Device_State),
+        (Input => (Config_State),
+         In_Out => (State, Device_State),
          Proof_In => (Init_State)),
-      Pre => Is_Initialized;
+      Pre => Is_Initialized,
+      Annotate =>
+        (GNATprove, Intentional,
+         "global input ""GMA.Config_State"" of ""Move_Cursor"" not read",
+         "Reading of Config_State depends on the platform configuration.");
 
    ----------------------------------------------------------------------------
 
@@ -191,8 +208,6 @@
          Proof_In => (Init_State)),
       Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
 
-   pragma Warnings (GNATprove, Off, "no check message justified by this",
-                    Reason => "see Annotate aspects.");
    procedure Map_Linear_FB (Linear_FB : out Word64; FB : in Framebuffer_Type)
    with
       Global =>