#
893e1146 |
|
02-Aug-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Extend floating-point support within the ARMv7 model. The model can be configured for VFPv2, VFPv3 or VFPv4. Most VFP instructions are modelled now but some are still missing, i.e.: • VCVT for fixed-point and half-precision. • VSTM and VLDM.
|
#
b3a33fbc |
|
12-Dec-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add assembly code entry points for some decompiler tools.
|
#
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).
|
#
e609174b |
|
16-Oct-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
The ARM-M0 model is now hooked up to the "core/fast" decompiler.
|
#
dd2c33fc |
|
14-Oct-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make the building of SPEC theorems more lazy (when using arm_progLib.arm_spec_hex).
|
#
8d08dc89 |
|
11-Oct-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Various updates/improvements to the decompiler tools.
|
#
e54aed22 |
|
07-Oct-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Reorganisation and improvements for the "fast" decompiler. Now tentatively called the "core" decompiler.
|