time: Juggle with types for proof
Helps with SPARK GPL 2017.
Change-Id: Idc0a038b132438be13aef496c41d15300069ed02
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/20257
Reviewed-by: Stefan Reinauer <stefan.reinauer@coreboot.org>
Tested-by: Stefan Reinauer <stefan.reinauer@coreboot.org>
Reviewed-by: Paul Menzel <paulepanter@users.sourceforge.net>
diff --git a/common/hw-time.adb b/common/hw-time.adb
index c1666a6..28db95d 100644
--- a/common/hw-time.adb
+++ b/common/hw-time.adb
@@ -55,7 +55,8 @@
MHz : constant T := Timer.Hz / 1_000_000;
Current : constant T := Timer.Raw_Value_Min;
begin
- return Int64 ((Current and (2 ** 63 - 1)) / (if MHz = 0 then 1 else MHz));
+ return Int64 (Current and (2 ** 63 - 1))
+ / Int64 (if MHz = 0 then T'(1) else MHz);
end Now_US;
----------------------------------------------------------------------------
