Add a facility for ignoring complex asm.

To restore some previous functionality, add a mechanism by which an __asm__
statement too complex to be translated can still be ignored (handled as an
empty statement). A demo file does this for a wrapper around "nop".

Also use this facility to support legacy camkes-glue proofs which assume
that the software interrupt operator "swi" doesn't break anything.

Handling of AsmStmt in c-parser, more tests.

The C-parser contains a full parser for __asm__ syntax but
up until now hasn't done anything with it. Instead we export
some semantics. It's unspecified exactly what these semantics
are but they are parametrised with the __asm__ semantics that
went in to them, so the translation validation has something
to reason about.

Tweak modifies proofs as a result, and add some more test files.

lib/spec/proof/tools: fix word change fallout

c-parser: fix architecture refactor bugs arising

- the symbol table constant had a hard map to word32 instead of the addr
alias
- when cast to integers, the parser believed pointers gave rise to 32
bit values. This latter required the TargetNumbers signature to get a
smidge wider, with a new ptr_t entry where the intptr type gets
listed.

Properly fix JIRA VER-439

The handling of local static variables is now part of a general
improvement in the handling of all the "munging" that the parser does.

*Munging* is the process of renaming variables so that Isabelle can cope
with them. There are at least three different forms of munging at the
moment:

- static locals get munged so that multiple static locals (which have to
be treated as globals) can co-exist with the same source name.
- local variables of the same source name but different types have to be
able to co-exist
- variables with legitimate C names but illegal Isabelle names have to
be allowed

The new structure MString implements an opaque version of string
designed to make it clear to the typechecker that certain strings are
"munged".

Fix for JIRA VER-429 (with test-case)

The null-pointer value was not being given the right type when a
comparison was made with the zero literal.

Port AutoCorres to Isabelle 2014-RC0

Import release snapshot.