gma config_helpers: Introduce Valid_FB()
Make the post condition of Validate_Config() a separate function,
Valid_FB(). This way, we don't have to repeat it everywhere.
Theoretically, we could make Validate_Config() an expression
function, too. Alas, all the added conditions seem to distract
provers too much.
Change-Id: I0931217658000d3ff6d71515acb45aeb063768d5
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/35527
Reviewed-by: Arthur Heymans <arthur@aheymans.xyz>
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
diff --git a/common/hw-gfx-gma-config_helpers.ads b/common/hw-gfx-gma-config_helpers.ads
index d56be5e..7bbf423 100644
--- a/common/hw-gfx-gma-config_helpers.ads
+++ b/common/hw-gfx-gma-config_helpers.ads
@@ -39,6 +39,18 @@
Reason => "Needed for older compiler versions");
use type HW.Pos32;
pragma Warnings (GNAT, On, """Integer_32"" is already use-visible *");
+
+ -- Validate just enough to satisfy Pipe_Setup pre conditions.
+ function Valid_FB
+ (FB : Framebuffer_Type;
+ Mode : Mode_Type)
+ return Boolean is
+ (Rotated_Width (FB) <= Mode.H_Visible and
+ Rotated_Height (FB) <= Mode.V_Visible and
+ (FB.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or
+ FB.Height + FB.Start_Y <= FB.V_Stride));
+
+ -- Also validate that we only use supported values / features.
function Validate_Config
(FB : Framebuffer_Type;
Mode : Mode_Type;
@@ -46,11 +58,6 @@
Scaler_Available : Boolean)
return Boolean
with
- Post =>
- (if Validate_Config'Result then
- Rotated_Width (FB) <= Mode.H_Visible and
- Rotated_Height (FB) <= Mode.V_Visible and
- (FB.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or
- FB.Height + FB.Start_Y <= FB.V_Stride));
+ Post => (if Validate_Config'Result then Valid_FB (FB, Mode));
end HW.GFX.GMA.Config_Helpers;