| #
aa23933d |
|
29-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Opening lcsymtacs is no longer necessary.
|
| #
0559f3bd |
|
14-Jul-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make use of alignmentTheory in the l3-machine-code examples.
|
| #
4069c0cd |
|
10-Feb-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Patches following commit 0e49bf8.
|
| #
bb4403ed |
|
15-Nov-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
The ARMv7 tools now support another memory representation.
Memory can now be treated as a map of type ``:word32 -> word32``.
Also reworked the tools with respect to the handling of word endianness.
|
| #
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).
|
| #
bc52f859 |
|
22-Oct-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Tool support for "LDR (literal)" under M0.
|
| #
44dc16f2 |
|
18-Oct-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Support for generating TEMPORAL triples.
Currently works for ARM, M0 and MIPS models. Yet to update the x86-64 model.
|
| #
a1e028ec |
|
02-Oct-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update M0 tools.
Minor updates to other ISA tools.
|
| #
40807410 |
|
27-Sep-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Further updates to the tools linking the L3 ARM model to the decompiler.
A lot of code has been generalised (making it usable with other models) and the performance has been improved.
|
| #
6c85649c |
|
16-Jul-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add ARM-M0 model (and tools) to examples.
|