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@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;