#
98874d92 |
|
04-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor update to an L3 lib file.
|
#
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.
|
#
ddee8978 |
|
12-May-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
L3 now supports the list update operation.
|
#
06401b70 |
|
18-Nov-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update for L3 machine-code examples. Some minor changes come from using the latest version of L3 when generating SML code. The ARMv8 model gains a function for encoding instructions (in the logic). The step tools are updated to support the NOP instruction.
|
#
a1b20d50 |
|
04-Mar-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update L3 import. Reverse can now operate over lists (and strings).
|
#
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
|