licenses: convert license tags to SPDX

asmrefine: Add support for 64-bit architectures.

asmrefine: update to Isabelle2019; reduce warnings

Isabelle2018: new AsmRefine session + test

Isabelle2018: new "op x" syntax; now is "(x)"

(result of "isabelle update_op -m <dir>")

Removes all trailing whitespaces

Support extra specs, ctzl, clzl in SimplExport.

This patch permits the user to supply additional specs for functions
whose bodies were not imported (DONT_TRANSLATE or not present in parsed
C source). Those specs are exported by SimplExport.

The existing apparatus can import builtin functions like ctzl/clzl in C
sources by admitting them without bodies (DONT_TRANSLATE) and giving
them axiomatic Hoare triples (FNSPEC).

Translation validation then requires export of useful semantics. The user
can supply a made-up body, and show that it is a refinement of the body
that the parser created (derived from the FNSPEC and MODIFIES clauses).
The body must export out the graph language correctly. For ctzl/clzl etc
this is easy.

SimplExportAndRefine: length 1 arrays.

This creates an issue because "unat x < 1" is reduced to "unat x = 0"
by the simplifier, meaning the unat_mono tactic doesn't get to operate on
it. The fix is pretty easy. Also includes some extra investigation material.

Isabelle2016-1: update references to renamed constants and facts

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.

Handle another operation in SimplExport.

Handle pointer comparison operations in SimplExport.

word_lib: adjust theory dependencies

Isabelle2016: SimplExportAndRefine updated for RC3

Repair SimplExport/GraphRefine.

Treat guarded_spec_body like Spec in asmrefine.

The parser now emits guarded_spec_body for underspecified functions,
not Spec. SimplExport now treats them the same.

Try to avoid emitting const-globals via memory.

Sometimes it's simpler to access an unknown field of a const
global by just computing the offset from its symbol in memory
and assuming the relevant words are in the .rodata section. But
for known fields, it's easier to just figure out what the
constant value is. This complicates the proof slightly, since
it has to guess which case it is in.

Space out the CFunDump.txt file.

It's much easier to read that way.

Repair merge.

Really add all necessary PGlobalValid assertions.

Progress on upgrading GraphRefine.

Needed to handle new concepts being exported from Simpl.

Update to SimplExport, fixes.

Really add all necessary PGlobalValid assertions.

WIP on WCET annotations.

asmrefine: 2015 udpate

more Isabelle2015 update; AInvs up to (excluding) Syscall_AI

also includes some global replacements

Restore global valid assertions in graph refine.

The global-object pointer validity assertion is now created at
export time, and the graph refine mechanism now proves them. It
seems they were forgotten about once again in adjusting the globals
logic.

Update graph-refine for StaticFun change, bugfix.

Fix asmrefine stuff for 2014 branch.

SIMPL->Graph proofs largely working.

More asmrefine work, global swapping ready.

release cleanup

Import release snapshot.