commit | 22173223f4d561746631bbe7099cd01293533e3f | [log] [tgz] |
---|---|---|
author | Nico Huber <nico.h@gmx.de> | Thu Dec 14 00:02:03 2023 +0100 |
committer | Nico Huber <nico.h@gmx.de> | Thu Dec 14 00:08:59 2023 +0100 |
tree | 5abe5f9c3fc2a1d77d02540baadaffbae2ddc915 | |
parent | cdc0351958b431adb1fe9fa39f6f21c63214d62f [diff] [blame] |
Work around gnatprove trouble with >64-bit range type
diff --git a/src/filo-blockdev.adb b/src/filo-blockdev.adb index 8658e05..5bb6732 100644 --- a/src/filo-blockdev.adb +++ b/src/filo-blockdev.adb
@@ -19,7 +19,7 @@ begin -- With 32-bit longs, the current C interface -- can't access more than 512 * 2 ** 32: - if Offset / BLOCK_SIZE > Blockdev_Length (unsigned_long'last) then + if Unsigned_64 (Offset / BLOCK_SIZE) > Unsigned_64 (unsigned_long'last) then Success := False; return; end if;