commit 7eb1350b711e513c76a44169fafa22a699b28e03
author Nico Huber <nico.huber@secunet.com> Mon Jun 04 14:42:13 2018 +0200
committer Nico Huber <nico.h@gmx.de> Fri Jun 08 14:45:28 2018 +0000
tree 70f4dcce0992a185a34be57355342e9dc6ecf983
parent 565f33b23e3e8e223702d07d768f9f2a11dd5686

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>

common/hw-gfx-edid.ads

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;