edid: Use expression functions to rely less on proof inlining
Change-Id: I7c116762c2b3fa366318b09e60d0e1945057eec6
Signed-off-by: Nico Huber <nico.huber@secunet.com>
Reviewed-on: https://review.coreboot.org/26843
Tested-by: Nico Huber <nico.h@gmx.de>
Reviewed-by: Arthur Heymans <arthur@aheymans.xyz>
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;