gma: Juggle with types of a precondition
Using the same type (Pos64) as in the actual calculation below, helps
current SPARK Pro to prove absence of overflows (SPARK GPL 2016 still
works too ofc).
Change-Id: Ifde556f9201f3333be0eb8566bf69b7f9df11277
Signed-off-by: Nico Huber <nico.huber@secunet.com>
Reviewed-on: https://review.coreboot.org/18809
Tested-by: Nico Huber <nico.h@gmx.de>
Reviewed-by: Arthur Heymans <arthur@aheymans.xyz>
diff --git a/common/hw-gfx-gma-pipe_setup.adb b/common/hw-gfx-gma-pipe_setup.adb
index 57344e4..256c7f5 100644
--- a/common/hw-gfx-gma-pipe_setup.adb
+++ b/common/hw-gfx-gma-pipe_setup.adb
@@ -147,7 +147,7 @@
function To_Bytes (Pixels : Width_Type) return Word32
with
- Pre => (Word32 (Pixels) <= Word32'Last / 4 / Word32 (BPC_Type'Last) * 8)
+ Pre => (Pos64 (Pixels) <= Pos64 (Word32'Last) / 4 / BPC_Type'Last * 8)
is
begin
return Word32 (Pos64 (Pixels) * 4 * Framebuffer.BPC / 8);