c-parser: VER-881: process more function calls.

Two kinds of function calls were escaping the analysis. The first is simple,
the ReturnFnCall statement type, which was a silly omission from before.

Function calls inside initialiser statements are a more difficult problem.
The simplest solution was to move the VER-881 calculation into a
post-processing phase once those function calls have been moved to statement
positions.

JIRA VER-881: avoid complex call lvals.

This scans for statement-level function calls which will have complex
lvalue translations, either because their lvalues are compound
expressions or because their function return type will be promoted to
be stored. It treats them like expression-level function calls, with
an additional call statement added (saving to a ret_ variable) and
the complex lvalue step treated like an assignment.

Standalone C parser: scan for unhandled ASM.

Adds an additional analysis option to the external C parser. This
will report about any asm statements that were encountered and could
not be properly handled.

[NO_PROOF]

c-parser: allow_underscore_idents flag added + examples [VER-619][NO_PROOF]

Tweak serial code, don't reference print.

The function print isn't in scope in the Isabelle environment.

Finish serialisation code for AST.

Start of AST-dump analysis for c-parser.

Give the standalone c-parser the facility to dump out its internal AST. Only
half finished, I got bored writing serialisers for the many syntax datatypes.

There has been some discussion about how to check whether an seL4 change
impacts verification. My thought was that the obvious thing to check is the
C-parser's AST. If this is unchanged, then further analyses must be unchanged.

c-parser: make munge_info available from standalone-parser

Specification of file to emit to is via command-line switch. Take the
opportunity to make comand-line processing be done via GetOpt library.

JIRA VER-473

Fix standalone parser in light of 344ed539

Handle cpp in both standalone and Isabelle parsers

Japheth's recent change (6f7c660cb) to error-reporting for the latter
broke the former. Refactor code so that old and new code can coexist.
Would just use Japheth's code in the purely SML version too, but it uses
Isabelle/ML libraries that I can't be bothered to recreate in SML.

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".

New option to standalone parser to just test the C grammar.

Without even typechecking, none of the later phases of the analysis
get run.

Allow user to control path to C preprocessor (or not use it entirely).

As per example, syntax is

declare [[cpp_path="path to file"]]

If the empty string is used as the value, then no preprocessor will be
called.

The standalone parser has also been adjusted so that you can it with

--cpp=path

or

--nocpp

options.

Closes JIRA issue VER-337

Import release snapshot.