2010/11/16 Roberto Bagnara <bagnara@cs.unipr.it>
Fabio,
I saw that we use ldexpl() twice in the floating_point branch.
However:
1) that function is not available on several platforms;
2) in both cases we pass an argument of type double
as the first argument;
3) it seems we use that function in a way that is not
conditional on the floating-point format(s)
involved.
When you have time, can you please look at this issue?
Thanks,
Roberto