#
0e6816f8 |
|
28-Aug-2018 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Floating-point changes. `fpX_to_value` is defined as `float_to_value o fpX_to_float` (previously this was called `fpX_to_real`, which was misleading) `fpX_to_real` is now defined as `float_to_real o fpX_to_float`. This change will break proofs that use the old names.
|
#
fc5a98a5 |
|
29-Nov-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Check for signalling NaNs in floating-point conversions.
|
#
218c07dc |
|
29-Nov-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add some more float-to-float functions to machine_ieeeTheory. Also add versions that output flags for the exception status.
|
#
c0502876 |
|
28-Jul-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Avoid potential UNCHANGED exception when evaluating 64-bit float operations. Problem identified by Yong Kiam.
|
#
037155db |
|
12-Jul-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update floating-point theory to specify exception flags for some operations. • The flags are: DivideByZero, InvalidOp, Overflow, Precision and Underflow. • The arithmetic operations now return a pair (flags and result). • Native (oracle) evaluation has been overhauled. It now only applies to some 64-bit machine_ieeeTheory operations directly. • The L3 Importer has been updated.
|
#
cad11df6 |
|
17-Feb-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improve handling of NaNs in binary_ieeeTheory. The choice of NaN is now a function of the operation being performed. Previously all instances of float_some_nan would be the same (for any given float type).
|
#
f8f368f9 |
|
10-Jun-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Revert "holyhammer: fix escaping of 0 and 1" This partially reverts commit 996d244090d790208dd6d865548a40acfb0e1e04. It seems like there were mistaken changes to an irrelevant file in that commit.
|
#
996d2440 |
|
10-Jun-2016 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
holyhammer: fix escaping of 0 and 1
|
#
bd1997ff |
|
26-Nov-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update for latest version of L3. Now supports floating-point square root and size conversions.
|
#
52264b7d |
|
01-May-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Relocate examples/l3-machine-code/common/fp to src/floating-point.
|