| #
27d6cfb0 |
|
27-Jun-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor update to some L3 models.
|
| #
d34415b5 |
|
02-May-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update for latest L3.
Removes some unnecessary bracketing.
|
| #
4b08982c |
|
03-Apr-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update for latest version of L3.
|
| #
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.
|
| #
f69520e1 |
|
16-Oct-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update model for latest version of L3.
|
| #
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.
|
| #
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.
|
| #
22ffb16d |
|
16-May-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Merge "_,_" instances in patterns.
|
| #
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
|