commit cf88f3d1567cf6475be5ddf3e7a433895a6144a6
author Nico Huber <nico.huber@secunet.com> Tue Jun 05 13:27:34 2018 +0200
committer Nico Huber <nico.h@gmx.de> Mon May 06 16:16:05 2019 +0000
tree 36ab3da2bffd540bfdfbb54e824ae57d6c40fb80
parent 67cf6d8f2bd36d8f78f48dfb927789d007b7740f

gma: Provide `Global` contracts for public procedures

We have to enforce a contract on Power_Up_VGA(), as it has no effect
on older hardware generations.

Change-Id: I13af0d90ff738e1eea5f8992718e00a6a09c4705
Signed-off-by: Nico Huber <nico.huber@secunet.com>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/26866
Reviewed-by: Arthur Heymans <arthur@aheymans.xyz>
Tested-by: Nico Huber <nico.h@gmx.de>

common/hw-gfx-gma.ads

diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 1f81ece..7f44a0f 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -16,6 +16,7 @@
 with HW.Config;
 with HW.Time;
 with HW.Port_IO;
+with HW.GFX.Framebuffer_Filler;
 
 package HW.GFX.GMA
 with
@@ -107,44 +108,86 @@
       Global => (Input => Init_State);
    pragma Warnings (GNATprove, On, "unused variable ""Write_Delay""");
 
-   pragma Warnings (GNATprove, Off, "subprogram ""Power_Up_VGA"" has no effect",
-                    Reason => "Effect depends on the platform compiled for");
    procedure Power_Up_VGA
    with
+      Global =>
+        (Input => (State, Time.State),
+         In_Out => (Device_State),
+         Proof_In => (Init_State)),
       Pre => Is_Initialized;
 
-   procedure Update_Outputs (Configs : Pipe_Configs);
+   ----------------------------------------------------------------------------
 
-   procedure Update_Cursor (Pipe : Pipe_Index; Cursor : Cursor_Type);
+   procedure Update_Outputs (Configs : Pipe_Configs)
+   with
+      Global =>
+        (Input => (Config_State, Time.State),
+         In_Out => (State, Device_State, Port_IO.State),
+         Proof_In => (Init_State)),
+      Pre => Is_Initialized;
+
+   procedure Update_Cursor (Pipe : Pipe_Index; Cursor : Cursor_Type)
+   with
+      Global =>
+        (In_Out => (State, Device_State),
+         Proof_In => (Init_State)),
+      Pre => Is_Initialized;
+
    procedure Place_Cursor
      (Pipe : Pipe_Index;
       X : Cursor_Pos;
-      Y : Cursor_Pos);
+      Y : Cursor_Pos)
+   with
+      Global =>
+        (In_Out => (State, Device_State),
+         Proof_In => (Init_State)),
+      Pre => Is_Initialized;
+
    procedure Move_Cursor
      (Pipe : Pipe_Index;
       X : Cursor_Pos;
-      Y : Cursor_Pos);
+      Y : Cursor_Pos)
+   with
+      Global =>
+        (In_Out => (State, Device_State),
+         Proof_In => (Init_State)),
+      Pre => Is_Initialized;
 
-   pragma Warnings (GNATprove, Off, "subprogram ""Dump_Configs"" has no effect",
-                    Reason => "It's only used for debugging");
-   procedure Dump_Configs (Configs : Pipe_Configs);
+   ----------------------------------------------------------------------------
 
    procedure Write_GTT
      (GTT_Page       : GTT_Range;
       Device_Address : GTT_Address_Type;
-      Valid          : Boolean);
+      Valid          : Boolean)
+   with
+      Global => (In_Out => Device_State, Proof_In => Init_State),
+      Pre => Is_Initialized;
 
    procedure Setup_Default_FB
      (FB       : in     Framebuffer_Type;
       Clear    : in     Boolean := True;
       Success  :    out Boolean)
    with
+      Global =>
+        (In_Out =>
+           (State, Device_State,
+            Framebuffer_Filler.State, Framebuffer_Filler.Base_Address),
+         Proof_In => (Init_State)),
       Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
 
    procedure Map_Linear_FB (Linear_FB : out Word64; FB : in Framebuffer_Type)
    with
+      Global =>
+        (In_Out => (State, Device_State),
+         Proof_In => (Init_State)),
       Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
 
+   ----------------------------------------------------------------------------
+
+   pragma Warnings (GNATprove, Off, "subprogram ""Dump_Configs"" has no effect",
+                    Reason => "It's only used for debugging");
+   procedure Dump_Configs (Configs : Pipe_Configs);
+
 private
 
    -- For the default framebuffer setup (see below) with 90 degree rotations,