<p>Nico Huber has uploaded this change for <strong>review</strong>.</p><p><a href="https://review.coreboot.org/26866">View Change</a></p><pre style="font-family: monospace,monospace; white-space: pre-wrap;">gma: Provide `Global` contracts for all public procedures<br><br>As Power_Up_VGA() has no effect on older generation, we need to fake<br>the contract in GMA.Power_And_Clocks.Power_Up().<br><br>Change-Id: I13af0d90ff738e1eea5f8992718e00a6a09c4705<br>Signed-off-by: Nico Huber <nico.huber@secunet.com><br>---<br>M common/g45/hw-gfx-gma-power_and_clocks.adb<br>M common/g45/hw-gfx-gma-power_and_clocks.ads<br>M common/hw-gfx-framebuffer_filler.adb<br>M common/hw-gfx-framebuffer_filler.ads<br>M common/hw-gfx-gma.adb<br>M common/hw-gfx-gma.ads<br>M common/ironlake/hw-gfx-gma-power_and_clocks_ironlake.adb<br>M common/ironlake/hw-gfx-gma-power_and_clocks_ironlake.ads<br>8 files changed, 90 insertions(+), 14 deletions(-)<br><br></pre><pre style="font-family: monospace,monospace; white-space: pre-wrap;">git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/66/26866/1</pre><pre style="font-family: monospace,monospace; white-space: pre-wrap;"><span>diff --git a/common/g45/hw-gfx-gma-power_and_clocks.adb b/common/g45/hw-gfx-gma-power_and_clocks.adb</span><br><span>index d6ee9f9..899f55b 100644</span><br><span>--- a/common/g45/hw-gfx-gma-power_and_clocks.adb</span><br><span>+++ b/common/g45/hw-gfx-gma-power_and_clocks.adb</span><br><span>@@ -47,4 +47,12 @@</span><br><span> end case;</span><br><span> end Initialize;</span><br><span> </span><br><span style="color: hsl(120, 100%, 40%);">+ procedure Power_Up (Old_Configs, New_Configs : Pipe_Configs)</span><br><span style="color: hsl(120, 100%, 40%);">+ with</span><br><span style="color: hsl(120, 100%, 40%);">+ SPARK_Mode => Off</span><br><span style="color: hsl(120, 100%, 40%);">+ is</span><br><span style="color: hsl(120, 100%, 40%);">+ begin</span><br><span style="color: hsl(120, 100%, 40%);">+ null;</span><br><span style="color: hsl(120, 100%, 40%);">+ end Power_Up;</span><br><span style="color: hsl(120, 100%, 40%);">+</span><br><span> end HW.GFX.GMA.Power_And_Clocks;</span><br><span>diff --git a/common/g45/hw-gfx-gma-power_and_clocks.ads b/common/g45/hw-gfx-gma-power_and_clocks.ads</span><br><span>index 8f6c13c..519e3fb 100644</span><br><span>--- a/common/g45/hw-gfx-gma-power_and_clocks.ads</span><br><span>+++ b/common/g45/hw-gfx-gma-power_and_clocks.ads</span><br><span>@@ -12,6 +12,8 @@</span><br><span> -- GNU General Public License for more details.</span><br><span> --</span><br><span> </span><br><span style="color: hsl(120, 100%, 40%);">+with HW.GFX.GMA.Registers;</span><br><span style="color: hsl(120, 100%, 40%);">+</span><br><span> private package HW.GFX.GMA.Power_And_Clocks is</span><br><span> </span><br><span> procedure Initialize;</span><br><span>@@ -22,7 +24,12 @@</span><br><span> </span><br><span> procedure Power_Set_To (Configs : Pipe_Configs) is null;</span><br><span> </span><br><span style="color: hsl(0, 100%, 40%);">- procedure Power_Up (Old_Configs, New_Configs : Pipe_Configs) is null;</span><br><span style="color: hsl(120, 100%, 40%);">+ -- Fake contract required to analyze GMA.Power_Up_VGA().</span><br><span style="color: hsl(120, 100%, 40%);">+ procedure Power_Up (Old_Configs, New_Configs : Pipe_Configs)</span><br><span style="color: hsl(120, 100%, 40%);">+ with</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (Input => (Time.State),</span><br><span style="color: hsl(120, 100%, 40%);">+ In_Out => (Registers.Register_State));</span><br><span> </span><br><span> procedure Power_Down (Old_Configs, Tmp_Configs, New_Configs : Pipe_Configs)</span><br><span> is null;</span><br><span>diff --git a/common/hw-gfx-framebuffer_filler.adb b/common/hw-gfx-framebuffer_filler.adb</span><br><span>index 250d903..29c7da6 100644</span><br><span>--- a/common/hw-gfx-framebuffer_filler.adb</span><br><span>+++ b/common/hw-gfx-framebuffer_filler.adb</span><br><span>@@ -17,6 +17,8 @@</span><br><span> pragma Elaborate_All (HW.MMIO_Range);</span><br><span> </span><br><span> package body HW.GFX.Framebuffer_Filler</span><br><span style="color: hsl(120, 100%, 40%);">+with</span><br><span style="color: hsl(120, 100%, 40%);">+ Refined_State => (State => FB.State, Base_Address => FB.Base_Address)</span><br><span> is</span><br><span> </span><br><span> type FB_Index is new Natural range</span><br><span>diff --git a/common/hw-gfx-framebuffer_filler.ads b/common/hw-gfx-framebuffer_filler.ads</span><br><span>index 228d43a..7ad3b79 100644</span><br><span>--- a/common/hw-gfx-framebuffer_filler.ads</span><br><span>+++ b/common/hw-gfx-framebuffer_filler.ads</span><br><span>@@ -19,6 +19,9 @@</span><br><span> use type HW.Int32;</span><br><span> </span><br><span> package HW.GFX.Framebuffer_Filler</span><br><span style="color: hsl(120, 100%, 40%);">+with</span><br><span style="color: hsl(120, 100%, 40%);">+ Abstract_State => ((State with External), Base_Address),</span><br><span style="color: hsl(120, 100%, 40%);">+ Initializes => Base_Address</span><br><span> is</span><br><span> </span><br><span> procedure Fill (Linear_FB : Word64; Framebuffer : Framebuffer_Type)</span><br><span>diff --git a/common/hw-gfx-gma.adb b/common/hw-gfx-gma.adb</span><br><span>index f135a5e..c9da0f2 100644</span><br><span>--- a/common/hw-gfx-gma.adb</span><br><span>+++ b/common/hw-gfx-gma.adb</span><br><span>@@ -18,8 +18,6 @@</span><br><span> with HW.PCI.Dev;</span><br><span> pragma Elaborate_All (HW.PCI.Dev);</span><br><span> </span><br><span style="color: hsl(0, 100%, 40%);">-with HW.GFX.Framebuffer_Filler;</span><br><span style="color: hsl(0, 100%, 40%);">-</span><br><span> with HW.GFX.GMA.Config;</span><br><span> with HW.GFX.GMA.Config_Helpers;</span><br><span> with HW.GFX.GMA.Registers;</span><br><span>diff --git a/common/hw-gfx-gma.ads b/common/hw-gfx-gma.ads</span><br><span>index 1f81ece..7f44a0f 100644</span><br><span>--- a/common/hw-gfx-gma.ads</span><br><span>+++ b/common/hw-gfx-gma.ads</span><br><span>@@ -16,6 +16,7 @@</span><br><span> with HW.Config;</span><br><span> with HW.Time;</span><br><span> with HW.Port_IO;</span><br><span style="color: hsl(120, 100%, 40%);">+with HW.GFX.Framebuffer_Filler;</span><br><span> </span><br><span> package HW.GFX.GMA</span><br><span> with</span><br><span>@@ -107,44 +108,86 @@</span><br><span> Global => (Input => Init_State);</span><br><span> pragma Warnings (GNATprove, On, "unused variable ""Write_Delay""");</span><br><span> </span><br><span style="color: hsl(0, 100%, 40%);">- pragma Warnings (GNATprove, Off, "subprogram ""Power_Up_VGA"" has no effect",</span><br><span style="color: hsl(0, 100%, 40%);">- Reason => "Effect depends on the platform compiled for");</span><br><span> procedure Power_Up_VGA</span><br><span> with</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (Input => (State, Time.State),</span><br><span style="color: hsl(120, 100%, 40%);">+ In_Out => (Device_State),</span><br><span style="color: hsl(120, 100%, 40%);">+ Proof_In => (Init_State)),</span><br><span> Pre => Is_Initialized;</span><br><span> </span><br><span style="color: hsl(0, 100%, 40%);">- procedure Update_Outputs (Configs : Pipe_Configs);</span><br><span style="color: hsl(120, 100%, 40%);">+ ----------------------------------------------------------------------------</span><br><span> </span><br><span style="color: hsl(0, 100%, 40%);">- procedure Update_Cursor (Pipe : Pipe_Index; Cursor : Cursor_Type);</span><br><span style="color: hsl(120, 100%, 40%);">+ procedure Update_Outputs (Configs : Pipe_Configs)</span><br><span style="color: hsl(120, 100%, 40%);">+ with</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (Input => (Config_State, Time.State),</span><br><span style="color: hsl(120, 100%, 40%);">+ In_Out => (State, Device_State, Port_IO.State),</span><br><span style="color: hsl(120, 100%, 40%);">+ Proof_In => (Init_State)),</span><br><span style="color: hsl(120, 100%, 40%);">+ Pre => Is_Initialized;</span><br><span style="color: hsl(120, 100%, 40%);">+</span><br><span style="color: hsl(120, 100%, 40%);">+ procedure Update_Cursor (Pipe : Pipe_Index; Cursor : Cursor_Type)</span><br><span style="color: hsl(120, 100%, 40%);">+ with</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (In_Out => (State, Device_State),</span><br><span style="color: hsl(120, 100%, 40%);">+ Proof_In => (Init_State)),</span><br><span style="color: hsl(120, 100%, 40%);">+ Pre => Is_Initialized;</span><br><span style="color: hsl(120, 100%, 40%);">+</span><br><span> procedure Place_Cursor</span><br><span> (Pipe : Pipe_Index;</span><br><span> X : Cursor_Pos;</span><br><span style="color: hsl(0, 100%, 40%);">- Y : Cursor_Pos);</span><br><span style="color: hsl(120, 100%, 40%);">+ Y : Cursor_Pos)</span><br><span style="color: hsl(120, 100%, 40%);">+ with</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (In_Out => (State, Device_State),</span><br><span style="color: hsl(120, 100%, 40%);">+ Proof_In => (Init_State)),</span><br><span style="color: hsl(120, 100%, 40%);">+ Pre => Is_Initialized;</span><br><span style="color: hsl(120, 100%, 40%);">+</span><br><span> procedure Move_Cursor</span><br><span> (Pipe : Pipe_Index;</span><br><span> X : Cursor_Pos;</span><br><span style="color: hsl(0, 100%, 40%);">- Y : Cursor_Pos);</span><br><span style="color: hsl(120, 100%, 40%);">+ Y : Cursor_Pos)</span><br><span style="color: hsl(120, 100%, 40%);">+ with</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (In_Out => (State, Device_State),</span><br><span style="color: hsl(120, 100%, 40%);">+ Proof_In => (Init_State)),</span><br><span style="color: hsl(120, 100%, 40%);">+ Pre => Is_Initialized;</span><br><span> </span><br><span style="color: hsl(0, 100%, 40%);">- pragma Warnings (GNATprove, Off, "subprogram ""Dump_Configs"" has no effect",</span><br><span style="color: hsl(0, 100%, 40%);">- Reason => "It's only used for debugging");</span><br><span style="color: hsl(0, 100%, 40%);">- procedure Dump_Configs (Configs : Pipe_Configs);</span><br><span style="color: hsl(120, 100%, 40%);">+ ----------------------------------------------------------------------------</span><br><span> </span><br><span> procedure Write_GTT</span><br><span> (GTT_Page : GTT_Range;</span><br><span> Device_Address : GTT_Address_Type;</span><br><span style="color: hsl(0, 100%, 40%);">- Valid : Boolean);</span><br><span style="color: hsl(120, 100%, 40%);">+ Valid : Boolean)</span><br><span style="color: hsl(120, 100%, 40%);">+ with</span><br><span style="color: hsl(120, 100%, 40%);">+ Global => (In_Out => Device_State, Proof_In => Init_State),</span><br><span style="color: hsl(120, 100%, 40%);">+ Pre => Is_Initialized;</span><br><span> </span><br><span> procedure Setup_Default_FB</span><br><span> (FB : in Framebuffer_Type;</span><br><span> Clear : in Boolean := True;</span><br><span> Success : out Boolean)</span><br><span> with</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (In_Out =></span><br><span style="color: hsl(120, 100%, 40%);">+ (State, Device_State,</span><br><span style="color: hsl(120, 100%, 40%);">+ Framebuffer_Filler.State, Framebuffer_Filler.Base_Address),</span><br><span style="color: hsl(120, 100%, 40%);">+ Proof_In => (Init_State)),</span><br><span> Pre => Is_Initialized and HW.Config.Dynamic_MMIO;</span><br><span> </span><br><span> procedure Map_Linear_FB (Linear_FB : out Word64; FB : in Framebuffer_Type)</span><br><span> with</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (In_Out => (State, Device_State),</span><br><span style="color: hsl(120, 100%, 40%);">+ Proof_In => (Init_State)),</span><br><span> Pre => Is_Initialized and HW.Config.Dynamic_MMIO;</span><br><span> </span><br><span style="color: hsl(120, 100%, 40%);">+ ----------------------------------------------------------------------------</span><br><span style="color: hsl(120, 100%, 40%);">+</span><br><span style="color: hsl(120, 100%, 40%);">+ pragma Warnings (GNATprove, Off, "subprogram ""Dump_Configs"" has no effect",</span><br><span style="color: hsl(120, 100%, 40%);">+ Reason => "It's only used for debugging");</span><br><span style="color: hsl(120, 100%, 40%);">+ procedure Dump_Configs (Configs : Pipe_Configs);</span><br><span style="color: hsl(120, 100%, 40%);">+</span><br><span> private</span><br><span> </span><br><span> -- For the default framebuffer setup (see below) with 90 degree rotations,</span><br><span>diff --git a/common/ironlake/hw-gfx-gma-power_and_clocks_ironlake.adb b/common/ironlake/hw-gfx-gma-power_and_clocks_ironlake.adb</span><br><span>index a7b1035..3bc1050 100644</span><br><span>--- a/common/ironlake/hw-gfx-gma-power_and_clocks_ironlake.adb</span><br><span>+++ b/common/ironlake/hw-gfx-gma-power_and_clocks_ironlake.adb</span><br><span>@@ -54,4 +54,12 @@</span><br><span> Config.Raw_Clock := Config.Default_RawClk_Freq;</span><br><span> end Initialize;</span><br><span> </span><br><span style="color: hsl(120, 100%, 40%);">+ procedure Power_Up (Old_Configs, New_Configs : Pipe_Configs)</span><br><span style="color: hsl(120, 100%, 40%);">+ with</span><br><span style="color: hsl(120, 100%, 40%);">+ SPARK_Mode => Off</span><br><span style="color: hsl(120, 100%, 40%);">+ is</span><br><span style="color: hsl(120, 100%, 40%);">+ begin</span><br><span style="color: hsl(120, 100%, 40%);">+ null;</span><br><span style="color: hsl(120, 100%, 40%);">+ end Power_Up;</span><br><span style="color: hsl(120, 100%, 40%);">+</span><br><span> end HW.GFX.GMA.Power_And_Clocks_Ironlake;</span><br><span>diff --git a/common/ironlake/hw-gfx-gma-power_and_clocks_ironlake.ads b/common/ironlake/hw-gfx-gma-power_and_clocks_ironlake.ads</span><br><span>index fc58d75..0e5f62d 100644</span><br><span>--- a/common/ironlake/hw-gfx-gma-power_and_clocks_ironlake.ads</span><br><span>+++ b/common/ironlake/hw-gfx-gma-power_and_clocks_ironlake.ads</span><br><span>@@ -12,6 +12,8 @@</span><br><span> -- GNU General Public License for more details.</span><br><span> --</span><br><span> </span><br><span style="color: hsl(120, 100%, 40%);">+with HW.GFX.GMA.Registers;</span><br><span style="color: hsl(120, 100%, 40%);">+</span><br><span> private package HW.GFX.GMA.Power_And_Clocks_Ironlake is</span><br><span> </span><br><span> procedure Initialize;</span><br><span>@@ -22,7 +24,12 @@</span><br><span> </span><br><span> procedure Power_Set_To (Configs : Pipe_Configs) is null;</span><br><span> </span><br><span style="color: hsl(0, 100%, 40%);">- procedure Power_Up (Old_Configs, New_Configs : Pipe_Configs) is null;</span><br><span style="color: hsl(120, 100%, 40%);">+ -- Fake contract required to analyze GMA.Power_Up_VGA().</span><br><span style="color: hsl(120, 100%, 40%);">+ procedure Power_Up (Old_Configs, New_Configs : Pipe_Configs)</span><br><span style="color: hsl(120, 100%, 40%);">+ with</span><br><span style="color: hsl(120, 100%, 40%);">+ Global =></span><br><span style="color: hsl(120, 100%, 40%);">+ (Input => (Time.State),</span><br><span style="color: hsl(120, 100%, 40%);">+ In_Out => (Registers.Register_State));</span><br><span> </span><br><span> procedure Power_Down (Old_Configs, Tmp_Configs, New_Configs : Pipe_Configs)</span><br><span> is null;</span><br><span></span><br></pre><p>To view, visit <a href="https://review.coreboot.org/26866">change 26866</a>. To unsubscribe, or for help writing mail filters, visit <a href="https://review.coreboot.org/settings">settings</a>.</p><div itemscope itemtype="http://schema.org/EmailMessage"><div itemscope itemprop="action" itemtype="http://schema.org/ViewAction"><link itemprop="url" href="https://review.coreboot.org/26866"/><meta itemprop="name" content="View Change"/></div></div>
<div style="display:none"> Gerrit-Project: libgfxinit </div>
<div style="display:none"> Gerrit-Branch: master </div>
<div style="display:none"> Gerrit-MessageType: newchange </div>
<div style="display:none"> Gerrit-Change-Id: I13af0d90ff738e1eea5f8992718e00a6a09c4705 </div>
<div style="display:none"> Gerrit-Change-Number: 26866 </div>
<div style="display:none"> Gerrit-PatchSet: 1 </div>
<div style="display:none"> Gerrit-Owner: Nico Huber <nico.h@gmx.de> </div>