I think you are asking for 1 more bit of precision than is actually available "under the hood".
Your declaration
type Fixed_Type is delta 1.0 / 2**32 range 0.0 .. 1.0
with Size => 32;
is only accepted because GNAT has used a biased representation; there's no room for a sign bit. You can see this because 0.7071067810
is represented as 16#B504F333#
, with the most significant bit set. So, when you multiply 0.71 by 0.71, the result has the most significant bit set; and the low-level code thinks that this must be the sign bit, so we have an overflow.
If you declare Fixed_Type
as
type Fixed_Type is delta 1.0 / 2**31 range 0.0 .. 1.0
with Size => 32;
all should be well.
A further point: in your report of the behaviour of specifics
with an input of 0.75, you quote the result
>>> 0.75
Value 0.7500000000 does not square properly.
Square: -0.4375000000
Not sure how that worked.
I rebuilt with gnatmake specifics.adb -g -gnato -bargs -E
, and the result is now
>>> 0.75
Value 0.7500000000 does not square properly.
Execution terminated by unhandled exception
Exception name: CONSTRAINT_ERROR
Message: 64-bit arithmetic overflow
Call stack traceback locations:
0x100020b79 0x10000ea80 0x100003520 0x100003912 0x10000143e
and the traceback decodes as
system__arith_64__raise_error (in specifics) (s-arit64.adb:364)
__gnat_mulv64 (in specifics) (s-arit64.adb:318)
specifics__testvalue.2581 (in specifics) (specifics.adb:20) <<<<<<<<<<
_ada_specifics (in specifics) (specifics.adb:45)
main (in specifics) (b~specifics.adb:246)
and specifics.adb:20
is
TIO.Put_Line("Square: " & Fixed_Type'Image(val * val));
in the exception handler, which involves the problematic square again (not a good thing to do in an exception handler). You can see that the value 0.75
was printed without any problem in the line above: and in fixedpointtest.adb
there was no problem in the additions leading to the last valid value 0.7071067810
.
I was rather surprised to find that -gnato
detects this error, since I'd thought it only applied to integer arithmetic; but in fact there's a discussion in the GNAT User Guide which states that it applies to fixed-point arithmetic too. It turns out that you can avoid the constraint error and get the correct arithmetic result by using -gnato3
:
>>> 0.75
Value 0.7500000000 squares properly.
Square: 0.5625000000
but only at the cost of using arbitrary multiple-precision arithmetic - not a good idea for a time-constrained system!