commit 8a5a3b5a0cdd368c17f103e4f84eff588b50111d
author Nico Huber <nico.huber@secunet.com> Mon Jun 04 14:42:13 2018 +0200
committer Nico Huber <nico.h@gmx.de> Wed Jun 13 08:58:13 2018 +0000
tree af4dbdf45b42f075312f778a662b8b212d6d69a4
parent 5a3191f6ef7a01b7a73442b4b6940fd7cf033fba

gma: Add contract to Enable_Output() to rely less on proof inlining

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

common/hw-gfx-gma.adb

diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb
index a5e9dbe..ab4e1e2 100644
--- a/common/hw-gfx-gma.adb
+++ b/common/hw-gfx-gma.adb
@@ -97,6 +97,8 @@
      (Pipe     : in     Pipe_Index;
       Pipe_Cfg : in     Pipe_Config;
       Success  :    out Boolean)
+   with
+      Pre => Pipe_Cfg.Port in Active_Port_Type
    is
       Port_Cfg : Port_Config;
       Scaler_Available : Boolean;