license-tool: missing license headers + .licenseignore [VER-551]

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

Handle local static variables properly.

They are now treated as globals with a specially munged name, derived
from the given name and the name of the function where they occur. The
function NameGeneration.mk_localstatic generates the "munged" name.

As with other globals, initialisation is not handled very well (i.e., at
the moment the initialisation is completely ignored).

Close JIRA VER-439

Start a test-case for JIRA VER-439 (static vars)