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


# 6ccca7af 16-Feb-2016 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Make more of the floating-point library available to Moscow ML users.

Evaluation now works under Poly/ML. However, Poly/ML is needed for evaluation
using native floats (which is controlled through the "native ieee" trace).