gfx, gma pipe_setup: Rewrite Scale_Keep_Aspect
Use Scaling_Type() to organize the different scaling cases. Looks better
and outlining the calculation helps GNATprove on bad days.
Change-Id: I14af765c6f17aeccff3f9274ccec3756493670d7
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/26848
Reviewed-by: Arthur Heymans <arthur@aheymans.xyz>
diff --git a/common/hw-gfx.ads b/common/hw-gfx.ads
index 86ef51b..beb111f 100644
--- a/common/hw-gfx.ads
+++ b/common/hw-gfx.ads
@@ -198,17 +198,22 @@
Rotated_Height (FB) /= Mode.V_Visible);
type Scaling_Aspect is (Uniform, Letterbox, Pillarbox);
- function Scaling_Type (FB : Framebuffer_Type; Mode : Mode_Type)
+ function Scaling_Type (Width, Height, Scaled_Width, Scaled_Height : Pos32)
return Scaling_Aspect is
- (if Pos32 (Mode.H_Visible) * Pos32 (Rotated_Height (FB)) <
- Pos32 (Mode.V_Visible) * Pos32 (Rotated_Width (FB))
- then
- Letterbox
- elsif Pos32 (Mode.H_Visible) * Pos32 (Rotated_Height (FB)) >
- Pos32 (Mode.V_Visible) * Pos32 (Rotated_Width (FB))
- then
- Pillarbox
- else
- Uniform);
+ (if Scaled_Width * Height < Scaled_Height * Width then Letterbox
+ elsif Scaled_Width * Height > Scaled_Height * Width then Pillarbox
+ else Uniform)
+ with
+ Pre =>
+ Width <= Pos32 (Pos16'Last) and
+ Height <= Pos32 (Pos16'Last) and
+ Scaled_Width <= Pos32 (Pos16'Last) and
+ Scaled_Height <= Pos32 (Pos16'Last);
+ function Scaling_Type (FB : Framebuffer_Type; Mode : Mode_Type)
+ return Scaling_Aspect is (Scaling_Type
+ (Width => Pos32 (Rotated_Width (FB)),
+ Height => Pos32 (Rotated_Height (FB)),
+ Scaled_Width => Pos32 (Mode.H_Visible),
+ Scaled_Height => Pos32 (Mode.V_Visible)));
end HW.GFX;