| #
17aa1139 |
|
08-May-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add tool support for working with ARM instructions MRS, MSR and RFE.
|
| #
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
|
| #
e5073aed |
|
04-Nov-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Updates for machine-code tools.
Added support for introducing SEP_ARRAY predicates for memory operations (applied to the ARM and M0 models).
|
| #
8d08dc89 |
|
11-Oct-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Various updates/improvements to the decompiler tools.
|
| #
08244dc4 |
|
08-Jul-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Missing files from last commit.
|