[coreboot-gerrit] Change in libgfxinit[master]: gma: Provide `Global` contracts for all public procedures
Nico Huber (Code Review)
gerrit at coreboot.org
Tue Jun 5 15:38:45 CEST 2018
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 at 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;
--
To view, visit https://review.coreboot.org/26866
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: I13af0d90ff738e1eea5f8992718e00a6a09c4705
Gerrit-Change-Number: 26866
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/20180605/6c93cfa9/attachment-0001.html>
More information about the coreboot-gerrit
mailing list