History log of /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/model/riscv.sig
Revision Date Author Comments
# 3a981fec 21-Sep-2017 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Add some whitespace to signature files.


# 161d7acc 02-Jul-2017 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Floating-point update.

• isSignallingNan predicate is added to machine_ieeeTheory.
• The RISC-V model is simplified in places (for DIV and REM).
• The L3 import is extended to cover more operations.


# 086cbeb8 22-Jun-2017 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Minor changes within floating-point theory.

• The operations float_negate1985 and float_abs1985 have been removed.
• Added a predicate float_is_signalling and renamed float_some_nan to float_some_qnan.
• Fixed problem with EQ_tm and GT_tm being swapped in binary_ieeeSyntax.


# d34415b5 02-May-2017 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Update for latest L3.

Removes some unnecessary bracketing.


# e3deee9f 11-Apr-2017 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Update RISC-V SML code.

Should have been included with commit 4b08982.


# 5835e692 27-May-2016 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Add SML version of RISC-V model.