| #
fdeae967 |
|
29-Apr-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update for the latest version of L3.
Changes have been made when exporting operations of the form:
`f : args -> state -> value * state`
If the state is not changed then this is now exported as
`f : args -> state -> value`
If the state is changed but the `value` type is `unit` then it this is now exported as
`f : args -> state -> state`.
|
| #
aa23933d |
|
29-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Opening lcsymtacs is no longer necessary.
|
| #
6ccd2dcc |
|
20-Oct-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update following 34d6b74.
|
| #
0559f3bd |
|
14-Jul-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make use of alignmentTheory in the l3-machine-code examples.
|
| #
7a4af63c |
|
26-Sep-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add support for the ARMv8 instruction CCMP (register).
This instruction was inadvertently left out (only the immediate variant was modelled). A few minor changes are made elsewhere.
|
| #
d2da74b7 |
|
12-Aug-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
ARMv8 model and tools.
This model supports AArch64 mode only, i.e. there's no support for the AArch32 mode.
|