History log of /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/arm_encoderLib.sig
Revision Date Author Comments
# 29126407 23-Jul-2010 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Minor change capturing unpredictable case for LDM -- from latest ARM reference
errata 7.

Changed the return type for functions provided by arm_parserLib and
arm_encoderLib. They now include a symbol table, which identifies the address
of labels.

Clean up following changes to EmitML. Also, some other tweaks wrt evaluation.


# 9241c39a 09-Sep-2009 Anthony Fox <anthony.fox@cl.cam.ac.uk>

A few refinements. Also added an examples file, which demonstrates how
to use armLib.


# 9dfee26e 18-Aug-2009 Anthony Fox <anthony.fox@cl.cam.ac.uk>

A new Monadic ARM instruction set specification. Covers all current ISA
versions i.e. ARMv4 to ARMv7.

Doesn't cover the ThumbEE, VFP and Advanced SIMD extensions. Also doesn't
model hardware interrupts - these will be added at a later date.

To use the armLib tools, Moscow ML users will likely have to apply the patch to
avoid the Chr exception.
<http://hol.sourceforge.net/mosml-chr-instructions.html>