[coreboot-gerrit] Change in libgfxinit[master]: gma: Add contract to Enable_Output() to rely less on proof inlining

[Nico Huber (Code Review)]

Nico Huber has uploaded this change for review. ( https://review.coreboot.org/26845


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

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

Change-Id: I7bc066b33c969e528c7bcd9328178fac8a37ad21
Signed-off-by: Nico Huber <nico.huber at secunet.com>
---
M common/hw-gfx-gma.adb
1 file changed, 2 insertions(+), 0 deletions(-)



  git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/45/26845/1

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;

-- 
To view, visit https://review.coreboot.org/26845
To unsubscribe, or for help writing mail filters, visit https://review.coreboot.org/settings

Gerrit-Project: libgfxinit
Gerrit-Branch: master
Gerrit-MessageType: newchange
Gerrit-Change-Id: I7bc066b33c969e528c7bcd9328178fac8a37ad21
Gerrit-Change-Number: 26845
Gerrit-PatchSet: 1
Gerrit-Owner: Nico Huber <nico.h at gmx.de>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.coreboot.org/pipermail/coreboot-gerrit/attachments/20180604/e333d782/attachment-0001.html>