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-pipe_setup.ads b/common/hw-gfx-gma-pipe_setup.ads
index 0edb0c9..3ecb6dd 100644
--- a/common/hw-gfx-gma-pipe_setup.ads
+++ b/common/hw-gfx-gma-pipe_setup.ads
@@ -13,6 +13,7 @@
--
with HW.GFX.GMA.Config;
+with HW.GFX.GMA.Config_Helpers;
with HW.GFX.GMA.Registers;
use type HW.Int32;
@@ -26,11 +27,7 @@
Framebuffer : Framebuffer_Type;
Cursor : Cursor_Type)
with
- Pre =>
- Rotated_Width (Framebuffer) <= Port_Cfg.Mode.H_Visible and
- Rotated_Height (Framebuffer) <= Port_Cfg.Mode.V_Visible and
- (Framebuffer.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or
- Framebuffer.Height + Framebuffer.Start_Y <= Framebuffer.V_Stride);
+ Pre => Config_Helpers.Valid_FB (Framebuffer, Port_Cfg.Mode);
procedure Off (Pipe : Pipe_Index);
@@ -43,11 +40,7 @@
Mode : Mode_Type;
Framebuffer : Framebuffer_Type)
with
- Pre =>
- Rotated_Width (Framebuffer) <= Mode.H_Visible and
- Rotated_Height (Framebuffer) <= Mode.V_Visible and
- (Framebuffer.Offset = VGA_PLANE_FRAMEBUFFER_OFFSET or
- Framebuffer.Height + Framebuffer.Start_Y <= Framebuffer.V_Stride);
+ Pre => Config_Helpers.Valid_FB (Framebuffer, Mode);
procedure Update_Cursor
(Pipe : Pipe_Index;