[coreboot-gerrit] Change in libgfxinit[master]: gma display probing: Provide Global contract for Scan_Ports()

[Nico Huber (Code Review)]

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

Change subject: gma display probing: Provide Global contract for Scan_Ports()
......................................................................

gma display probing: Provide Global contract for Scan_Ports()

Change-Id: Ic3e342fb111a8b6f2ddb01b308b70eda7dd23413
Signed-off-by: Nico Huber 
---
M common/hw-gfx-gma-display_probing.adb
M common/hw-gfx-gma-display_probing.ads
2 files changed, 18 insertions(+), 1 deletion(-)

git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/67/26867/1

diff --git a/common/hw-gfx-gma-display_probing.adb b/common/hw-gfx-gma-display_probing.adb
index 9f756f6..d02d0e0 100644
--- a/common/hw-gfx-gma-display_probing.adb
+++ b/common/hw-gfx-gma-display_probing.adb
@@ -20,6 +20,7 @@
 with HW.GFX.GMA.DP_Aux_Ch;
 with HW.GFX.GMA.Panel;
 with HW.GFX.GMA.Power_And_Clocks;
+with HW.GFX.GMA.Registers;

with HW.Debug;
 with GNAT.Source_Info;
@@ -161,6 +162,14 @@
       Ports       : in     Port_List := All_Ports;
       Max_Pipe    : in     Pipe_Index := Pipe_Index'Last;
       Keep_Power  : in     Boolean := False)
+   with
+      Refined_Global =>
+        (Input =>
+           (GMA.Cur_Configs,
+            Config.Raw_Clock, Config.Valid_Port_GPU,
+            Time.State),
+         In_Out => (Panel.Panel_State, Registers.Register_State),
+         Proof_In => (Init_State))
    is
       Probe_Internal : Boolean := False;

diff --git a/common/hw-gfx-gma-display_probing.ads b/common/hw-gfx-gma-display_probing.ads
index f5cd839..8ad4acc 100644
--- a/common/hw-gfx-gma-display_probing.ads
+++ b/common/hw-gfx-gma-display_probing.ads
@@ -12,6 +12,8 @@
 -- GNU General Public License for more details.
 --

+with HW.Time;
+
 package HW.GFX.GMA.Display_Probing
 is

@@ -24,6 +26,12 @@
      (Configs     :    out Pipe_Configs;
       Ports       : in     Port_List := All_Ports;
       Max_Pipe    : in     Pipe_Index := Pipe_Index'Last;
-      Keep_Power  : in     Boolean := False);
+      Keep_Power  : in     Boolean := False)
+   with
+      Global =>
+        (Input => (GMA.Config_State, Time.State),
+         In_Out => (GMA.State, GMA.Device_State),
+         Proof_In => (GMA.Init_State)),
+      Pre => GMA.Is_Initialized;

end HW.GFX.GMA.Display_Probing;