time: Rewrite Now_US() again to ease automatic proving
Currently it struggles with the 64-bit modular to range conversion.
Adding a step in between, a 63-bit modular type, works better.
Change-Id: I32b1a771b18bcc243244cb05636dae6d9f148f90
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.sourcearcade.org/c/libhwbase/+/501
Tested-by: Ada SPARK <gnatbot@sourcearcade.org>
diff --git a/common/hw-time.adb b/common/hw-time.adb
index 42c63f6..b2fa564 100644
--- a/common/hw-time.adb
+++ b/common/hw-time.adb
@@ -54,11 +54,11 @@
Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
is
Hz : constant T := Timer.Hz;
- MHz : constant T := Hz / 1_000_000;
+ MHz : constant T := (if Hz >= 1_000_000 then Hz / 1_000_000 else 1);
Current : constant T := Timer.Raw_Value_Min;
+ type Word63 is mod 2 ** 63;
begin
- return Int64 (Current and (2 ** 63 - 1))
- / Int64 (if MHz = 0 then T'(1) else MHz);
+ return Int64 (Word63 ((Current and 2 ** 63 - 1) / MHz));
end Now_US;
----------------------------------------------------------------------------