commit e317e9c31cef31f960a5cfb3e3247047d39ae7a1
author Nico Huber <nico.h@gmx.de> Sun Sep 29 03:03:18 2019 +0200
committer Nico Huber <nico.h@gmx.de> Fri Oct 04 22:18:44 2019 +0000
tree e995dd0feb54d1897d5e02b068d0838deb1ee493
parent c5c66ecf12c51600a20aac257394fd7f13d25113

gma: Merge `Config_State` into `State`

Treating `Config_State` separately was merely cosmetic and caused
lots of trouble. Its usage depends heavily on the selected plat-
form. Hence, `Global` contracts were not stable across different
configurations.

Let's avoid the annotation mess that it brought us and merge it
into `State`.

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

common/hw-gfx-gma.ads

diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads
index 3a4580e..bdc4704 100644
--- a/common/hw-gfx-gma.ads
+++ b/common/hw-gfx-gma.ads
@@ -24,7 +24,6 @@
    Abstract_State =>
      (State,
       Init_State,
-      Config_State,
       (Device_State with External)),
    Initializes => Init_State
 is
@@ -105,7 +104,7 @@
    with
       Global =>
         (In_Out => (Device_State, Port_IO.State),
-         Output => (State, Init_State, Config_State),
+         Output => (State, Init_State),
          Input  => (Time.State)),
       Post => Success = Is_Initialized;
    function Is_Initialized return Boolean
@@ -116,7 +115,7 @@
    procedure Power_Up_VGA
    with
       Global =>
-        (Input => (State, Config_State, Time.State),
+        (Input => (State, Time.State),
          In_Out => (Device_State),
          Proof_In => (Init_State)),
       Pre => Is_Initialized;
@@ -126,24 +125,17 @@
    procedure Update_Outputs (Configs : Pipe_Configs)
    with
       Global =>
-        (Input => (Config_State, Time.State),
+        (Input => (Time.State),
          In_Out => (State, Device_State, Port_IO.State),
          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 =>
-        (Input => (Config_State),
-         In_Out => (State, Device_State),
+        (In_Out => (State, Device_State),
          Proof_In => (Init_State)),
-      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.");
+      Pre => Is_Initialized;
 
    procedure Place_Cursor
      (Pipe : Pipe_Index;
@@ -151,14 +143,9 @@
       Y : Cursor_Pos)
    with
       Global =>
-        (Input => (Config_State),
-         In_Out => (State, Device_State),
+        (In_Out => (State, Device_State),
          Proof_In => (Init_State)),
-      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.");
+      Pre => Is_Initialized;
 
    procedure Move_Cursor
      (Pipe : Pipe_Index;
@@ -166,14 +153,9 @@
       Y : Cursor_Pos)
    with
       Global =>
-        (Input => (Config_State),
-         In_Out => (State, Device_State),
+        (In_Out => (State, Device_State),
          Proof_In => (Init_State)),
-      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.");
+      Pre => Is_Initialized;
 
    ----------------------------------------------------------------------------
 
@@ -183,7 +165,7 @@
       Valid          : Boolean)
    with
       Global =>
-        (Input => Config_State,
+        (Input => State,
          In_Out => Device_State, Proof_In => Init_State),
       Pre => Is_Initialized;
 
@@ -193,7 +175,7 @@
       GTT_Page       : in     GTT_Range)
    with
       Global =>
-        (Input => Config_State,
+        (Input => State,
          In_Out => Device_State, Proof_In => Init_State),
       Pre => Is_Initialized;
 
@@ -203,8 +185,7 @@
       Success  :    out Boolean)
    with
       Global =>
-        (Input => Config_State,
-         In_Out =>
+        (In_Out =>
            (State, Device_State,
             Framebuffer_Filler.State, Framebuffer_Filler.Base_Address),
          Proof_In => (Init_State)),
@@ -213,15 +194,9 @@
    procedure Map_Linear_FB (Linear_FB : out Word64; FB : in Framebuffer_Type)
    with
       Global =>
-        (Input => Config_State,
-         In_Out => (State, Device_State),
+        (In_Out => (State, Device_State),
          Proof_In => (Init_State)),
-      Pre => Is_Initialized and HW.Config.Dynamic_MMIO,
-      Annotate =>
-        (GNATprove, Intentional,
-         "global input ""GMA.Config_State"" of ""Map_Linear_FB"" not read",
-         "Reading of Config_State depends on the platform configuration.");
-   pragma Warnings (GNATprove, On, "no check message justified by this");
+      Pre => Is_Initialized and HW.Config.Dynamic_MMIO;
 
    ----------------------------------------------------------------------------