| #
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.
|
| #
d7726677 |
|
15-Feb-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update L3 examples.
Most changes relate to Poly/ML moving to fixed-width integers.
|
| #
6f3f50f2 |
|
27-Nov-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Further support for L3 floating-point.
|
| #
6a7534d9 |
|
27-Nov-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update L3 "lib" files.
|
| #
8f1ae54e |
|
15-Jul-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update SML files generated by L3.
The BitsN library has been sped up by removing word size checks.
|
| #
cc9dd295 |
|
21-Feb-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add assembly code parsing/printing support for the M0 and ARMv7 models.
There are new entry points to the decompiler. These take a function that maps a quotation (containing machine or assembly code) into a list of strings (typically hex). This facilitate the input of ARM assembly code. For example, the functions:
m0_decompLib.m0_decompile_code
m0_core_decompLib.m0_core_decompile_code
arm_decompLib.arm_decompile_code
arm_core_decompLib.arm_core_decompile_code
are provided with type
: string -> string quotation -> Thm.thm * Thm.thm
|