History log of /seL4-l4v-master/HOL4/src/floating-point/machine_ieeeScript.sml
Revision Date Author Comments
# 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.