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.

Opening lcsymtacs is no longer necessary.

Make use of alignmentTheory in the l3-machine-code examples.

Patches following commit 0e49bf8.

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.

Updates for machine-code tools.

Added support for introducing SEP_ARRAY predicates for memory operations (applied to the ARM and M0 models).

Tool support for "LDR (literal)" under M0.

Support for generating TEMPORAL triples.

Currently works for ARM, M0 and MIPS models. Yet to update the x86-64 model.

Updates and improvements to the l3-machine-code decompilation tools.

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.

The Hoare-triples for PC-relative loads now have immediate values appearing in the code-pool.

This affects the triples that are generated for instruction such as "ldr r1, [pc, #12]".

The tools for the other ISA models need minor updates following changes in stateLib.

Missing files from last commit.