gma pipe_setup: Replace helper function w/ assertions
The Scale() function was supposed to help with the proof but right now
(w/ gnatprove 11.2) it doesn't. The manual assertions don't seem to be
more fragile and get the job done.
Change-Id: Ib623d7b0b3f39c8157200d714a7951a89122bd9f
Signed-off-by: Nico Huber <nico.huber@secunet.com>
Reviewed-on: https://review.sourcearcade.org/c/libgfxinit/+/498
Tested-by: Nico Huber <nico.h@gmx.de>
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
diff --git a/common/hw-gfx-gma-pipe_setup.adb b/common/hw-gfx-gma-pipe_setup.adb
index 03aaf12..69d83a8 100644
--- a/common/hw-gfx-gma-pipe_setup.adb
+++ b/common/hw-gfx-gma-pipe_setup.adb
@@ -423,12 +423,6 @@
----------------------------------------------------------------------------
- function Scale (Val, Max, Num, Denom : Width_Type)
- return Width_Type is ((Val * Num) / Denom)
- with
- Pre => Denom <= Num and Val * Num < Max * Denom,
- Post => Scale'Result < Max;
-
procedure Scale_Keep_Aspect
(Width : out Width_Type;
Height : out Height_Type;
@@ -447,10 +441,14 @@
begin
case Scaling_Type (Src_Width, Src_Height, Max_Width, Max_Height) is
when Letterbox =>
+ Height := (Src_Height * Max_Width) / Src_Width;
+ pragma Assert (Height <= Max_Height);
Width := Max_Width;
- Height := Scale (Src_Height, Max_Height, Max_Width, Src_Width);
when Pillarbox =>
- Width := Scale (Src_Width, Max_Width, Max_Height, Src_Height);
+ Width := (Src_Width * Max_Height) / Src_Height;
+ pragma Assert (Max_Height * Src_Width < Max_Width * Src_Height);
+ pragma Assert ((Max_Height * Src_Width) / Src_Height < Max_Width);
+ pragma Assert (Width <= Max_Width);
Height := Max_Height;
when Uniform =>
Width := Max_Width;