[coreboot-gerrit] Change in libgfxinit[master]: edid: Use expression functions to rely less on proof inlining
Nico Huber (Code Review)
gerrit at coreboot.org
Mon Jun 4 22:48:14 CEST 2018
Nico Huber has uploaded this change for review. ( https://review.coreboot.org/26843
Change subject: edid: Use expression functions to rely less on proof inlining
......................................................................
edid: Use expression functions to rely less on proof inlining
Change-Id: I7c116762c2b3fa366318b09e60d0e1945057eec6
Signed-off-by: Nico Huber <nico.huber at secunet.com>
---
M common/hw-gfx-edid.adb
M common/hw-gfx-edid.ads
2 files changed, 29 insertions(+), 87 deletions(-)
git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/43/26843/1
diff --git a/common/hw-gfx-edid.adb b/common/hw-gfx-edid.adb
index f6afb56..83e9cf6 100644
--- a/common/hw-gfx-edid.adb
+++ b/common/hw-gfx-edid.adb
@@ -108,30 +108,6 @@
Word16 (Raw_EDID (Offset));
end Read_LE16;
- function Has_Preferred_Mode (Raw_EDID : Raw_EDID_Data) return Boolean
- is
- begin
- return
- Int64 (Read_LE16 (Raw_EDID, DESCRIPTOR_1)) * 10_000
- in Frequency_Type and
- ( Raw_EDID (DESCRIPTOR_1 + 2) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 4) and 16#f0#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 8) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#c0#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 9) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#30#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 3) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 4) and 16#0f#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 5) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 7) and 16#f0#) /= 0) and
- ((Raw_EDID (DESCRIPTOR_1 + 10) and 16#f0#) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#0c#) /= 0) and
- ((Raw_EDID (DESCRIPTOR_1 + 10) and 16#0f#) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#03#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 6) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 7) and 16#0f#) /= 0);
- end Has_Preferred_Mode;
-
function Preferred_Mode (Raw_EDID : Raw_EDID_Data) return Mode_Type
is
Base : constant := DESCRIPTOR_1;
@@ -140,38 +116,25 @@
function Read_12
(Lower_8, Upper_4 : Raw_EDID_Index;
Shift : Natural)
- return Word16
- is
- begin
- return
- Word16 (Raw_EDID (Lower_8)) or
- (Shift_Left (Word16 (Raw_EDID (Upper_4)), Shift) and 16#0f00#);
- end Read_12;
+ return Word16 is
+ ( Word16 (Raw_EDID (Lower_8)) or
+ (Shift_Left (Word16 (Raw_EDID (Upper_4)), Shift) and 16#0f00#));
function Read_10
(Lower_8, Upper_2 : Raw_EDID_Index;
Shift : Natural)
- return Word16
- is
- begin
- return
- Word16 (Raw_EDID (Lower_8)) or
- (Shift_Left (Word16 (Raw_EDID (Upper_2)), Shift) and 16#0300#);
- end Read_10;
+ return Word16 is
+ ( Word16 (Raw_EDID (Lower_8)) or
+ (Shift_Left (Word16 (Raw_EDID (Upper_2)), Shift) and 16#0300#));
function Read_6
(Lower_4 : Raw_EDID_Index;
Lower_Shift : Natural;
Upper_2 : Raw_EDID_Index;
Upper_Shift : Natural)
- return Word8
- is
- begin
- return
- (Shift_Right (Word8 (Raw_EDID (Lower_4)), Lower_Shift) and 16#0f#)
- or
- (Shift_Left (Word8 (Raw_EDID (Upper_2)), Upper_Shift) and 16#30#);
- end Read_6;
+ return Word8 is
+ ((Shift_Right (Word8 (Raw_EDID (Lower_4)), Lower_Shift) and 16#0f#) or
+ (Shift_Left (Word8 (Raw_EDID (Upper_2)), Upper_Shift) and 16#30#));
begin
Mode := Mode_Type'
(Dotclock => Pos64 (Read_LE16 (Raw_EDID, Base)) * 10_000,
diff --git a/common/hw-gfx-edid.ads b/common/hw-gfx-edid.ads
index abbb2ee..0d73230 100644
--- a/common/hw-gfx-edid.ads
+++ b/common/hw-gfx-edid.ads
@@ -42,49 +42,28 @@
with
Pre => Valid (Raw_EDID);
- function Has_Preferred_Mode (Raw_EDID : Raw_EDID_Data) return Boolean
+ function Has_Preferred_Mode (Raw_EDID : Raw_EDID_Data) return Boolean is
+ (Int64 (Read_LE16 (Raw_EDID, DESCRIPTOR_1)) * 10_000 in Frequency_Type and
+ ( Raw_EDID (DESCRIPTOR_1 + 2) /= 0 or
+ (Raw_EDID (DESCRIPTOR_1 + 4) and 16#f0#) /= 0) and
+ ( Raw_EDID (DESCRIPTOR_1 + 8) /= 0 or
+ (Raw_EDID (DESCRIPTOR_1 + 11) and 16#c0#) /= 0) and
+ ( Raw_EDID (DESCRIPTOR_1 + 9) /= 0 or
+ (Raw_EDID (DESCRIPTOR_1 + 11) and 16#30#) /= 0) and
+ ( Raw_EDID (DESCRIPTOR_1 + 3) /= 0 or
+ (Raw_EDID (DESCRIPTOR_1 + 4) and 16#0f#) /= 0) and
+ ( Raw_EDID (DESCRIPTOR_1 + 5) /= 0 or
+ (Raw_EDID (DESCRIPTOR_1 + 7) and 16#f0#) /= 0) and
+ ((Raw_EDID (DESCRIPTOR_1 + 10) and 16#f0#) /= 0 or
+ (Raw_EDID (DESCRIPTOR_1 + 11) and 16#0c#) /= 0) and
+ ((Raw_EDID (DESCRIPTOR_1 + 10) and 16#0f#) /= 0 or
+ (Raw_EDID (DESCRIPTOR_1 + 11) and 16#03#) /= 0) and
+ ( Raw_EDID (DESCRIPTOR_1 + 6) /= 0 or
+ (Raw_EDID (DESCRIPTOR_1 + 7) and 16#0f#) /= 0))
with
- Pre => Valid (Raw_EDID),
- Post =>
- (Has_Preferred_Mode'Result =
- (Int64 (Read_LE16 (Raw_EDID, DESCRIPTOR_1)) * 10_000
- in Frequency_Type and
- ( Raw_EDID (DESCRIPTOR_1 + 2) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 4) and 16#f0#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 8) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#c0#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 9) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#30#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 3) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 4) and 16#0f#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 5) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 7) and 16#f0#) /= 0) and
- ((Raw_EDID (DESCRIPTOR_1 + 10) and 16#f0#) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#0c#) /= 0) and
- ((Raw_EDID (DESCRIPTOR_1 + 10) and 16#0f#) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#03#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 6) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 7) and 16#0f#) /= 0)));
+ Pre => Valid (Raw_EDID);
function Preferred_Mode (Raw_EDID : Raw_EDID_Data) return Mode_Type
with
- Pre =>
- Int64 (Read_LE16 (Raw_EDID, DESCRIPTOR_1)) * 10_000
- in Frequency_Type and
- ( Raw_EDID (DESCRIPTOR_1 + 2) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 4) and 16#f0#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 8) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#c0#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 9) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#30#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 3) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 4) and 16#0f#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 5) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 7) and 16#f0#) /= 0) and
- ((Raw_EDID (DESCRIPTOR_1 + 10) and 16#f0#) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#0c#) /= 0) and
- ((Raw_EDID (DESCRIPTOR_1 + 10) and 16#0f#) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 11) and 16#03#) /= 0) and
- ( Raw_EDID (DESCRIPTOR_1 + 6) /= 0 or
- (Raw_EDID (DESCRIPTOR_1 + 7) and 16#0f#) /= 0);
+ Pre => Valid (Raw_EDID) and then Has_Preferred_Mode (Raw_EDID);
end HW.GFX.EDID;
--
To view, visit https://review.coreboot.org/26843
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: I7c116762c2b3fa366318b09e60d0e1945057eec6
Gerrit-Change-Number: 26843
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/20180604/f61f9342/attachment-0001.html>
More information about the coreboot-gerrit
mailing list