commit 86445f36097b75f3c1648868b72f9359937511d3
author Nico Huber <nico.h@gmx.de> Sun Jun 10 00:32:26 2018 +0200
committer Nico Huber <nico.h@gmx.de> Wed May 08 12:32:10 2019 +0000
tree db78c0eb2aff03a8dd9abe9c5626b13a39858812
parent 63ec8364dc2af8806ac1f52d806a2360128eb07e

gma pipe setup: Drop explicit Global and Depends contracts

These were originally only added to prevent proof inlining and
are not needed any more.

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

common/hw-gfx-gma-pipe_setup.adb

diff --git a/common/hw-gfx-gma-pipe_setup.adb b/common/hw-gfx-gma-pipe_setup.adb
index a237de7..76051dd 100644
--- a/common/hw-gfx-gma-pipe_setup.adb
+++ b/common/hw-gfx-gma-pipe_setup.adb
@@ -283,18 +283,6 @@
       Dither_BPC  : BPC_Type;
       Dither      : Boolean)
    with
-      Global => (In_Out => (Registers.Register_State, Port_IO.State)),
-      Depends =>
-        (Registers.Register_State
-            =>+
-              (Registers.Register_State,
-               Controller,
-               Framebuffer,
-               Dither_BPC,
-               Dither),
-         Port_IO.State
-            =>+
-               (Framebuffer)),
       Pre =>
          Framebuffer.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or
          Framebuffer.Height + Framebuffer.Start_Y <= Framebuffer.V_Stride