cparser: set sorry_modifies_proofs conditionally on env var

This includes replacing the non-thread-safe ref sorry_modifies_proofs with a
proper Config option.

Isabelle2017: remove String_Compare

This was a workaround for an Isabelle2016-1 performace regression, and
is no longer required.

c-parser: refactor arch-specific array memory model

This places all arch-specific aspects of the array memory
model in ArchArraysmemInstance.thy.

x64: add new modifies prover

Modifies proofs now include a preprocessing step which breaks programs
into parts before passing goals to the VCG. This means there are more
calls to the VCG, but the VCG only sees individual Basic and Spec
commands, and procedure calls.

This avoids performance issues in some pathological cases. In
particular, long sequences of updates to arrays via pointer-to-struct
previously seemed to be exponential in the number of updates.

x64: configure arch-specific array types

Isabelle2016-1: configure c-parser with faster string comparisons

c-parser: fix list sorting to use Isabelle code

This makes the licensing situation clearer than with the code coming
from Moscow ML (which might conceivably be GPL).

c-parser: sort munge output

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

Translate spec-only fns with new guarded_spec_body const

As per discussion in JIRA VER-464 issue.

Still to try to prove modifies theorems for such functions
automatically.

Define RelSpec bodies for DONT_TRANSLATE functions.

Work for JIRA VER-464

C-Parser 2015 update

c-parser: Add config option to avoid generating modifies proofs.

c-parser: Generate vcg rule for "cchaos" constant.

Allows vcg_tag ("apply vcg") to process functions with "cchaos" in them.

This was an attempt to solve the problem that the C parser's modifies
proofs currently fail for functions containing "cchaos".

The problem, however, actually seems to be that the C parser fails to
realise that incorrectly owned _read_ variables (which are updated using
"cchaos" before being read) need to be in the "modifies" set of
a function. Currently, the C parser misses these modifications, and the
proof of the incorrect modifies set (rightly) fails.

Renovate StaticFun a bit.

The functor is gone, and instead StaticFun exports two more general
operators, one for defining a partial map by a tree, and one for
extracting the theorems from an existing partial map definition.

The extraction process uses simplification in a more conservative
manner than before, and is guaranteed to produce exactly the
expected theorems.

Import release snapshot.