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