Document 'complex loop' aborts unconditionally.

Handle missing symbols as problem aborts.

Previously missing symbols resulted in a global failure, now only
the relevant problems will fail. This better suits a regression-test
approach which hopes to converge on correctness gradually.

Some more inner loop handling sanity.

This gets us past the 'check' phase of problem setup for functions
with inner loops.

Two major tweaks to var cycle analysis.

Firstly, var cycle analysis is now generally much better at handling
masking problems, e.g. when a linear variable is repeatedly masked off
or cast up and down, interspersed with other arithmetic.

Secondly, var cycle analysis detects dead paths within loops with some
vague approximation of const-propagation, which in particular allows an
offset value pageBitsForSize (SectionBits) in map_kernel_window to be
recognised as a constant offset.

Move consider_inline process to check.

It's still not really where it belongs. Really the target should specify
what the inlining process should be, but that breaks backward compatibility
a bit too much for me right now.

Tweak detection of complex loops.

Get function limit bounds working.

Resolution:
- the previous hack for general splittable points was restored.
- the loop bound function limit code was rewritten to not require
this anyway.

Adjust approach to splittables.

Generate splittable information lazily and store in cached_analysis
of problem. Also check for complex loops at a slightly different
point.

Also replace an experimental better split point detector in logic
with another experimental one which also doesn't work perfectly yet.

Search performance improvements.

Tweaking now, less tracing, more caching, more caution in using the
necessary linear sequence alignment, and a cache to avoid repeatedly
testing similar weakly aligned splits.

Tweak handling of reachability.

Move reachability cache to problem (from rep_graph), use in check
to insist on discovering (0) loop bounds slightly less often.

Initial switch-optimisation implementation.

Partly working. Has detection for switch-like problems that can probably
be best addressed with an initial case split. New search feature discovers
matching path pairs from within the case split set. Hook for building proofs
based on this not currently working.

Support dmb instruction and an accumulator.

For unrolled loops, we may need an accumulator where a value is incremented and
trimmed to 8-bits repeatedly. Bleh.

More support for inline scripts.

Activate inst_logic for seL4-example, fixups.

Minor adjustments.

bugfixes

Respect 'do_analysis = False' in inline_at_point.

Faster problem (re-)construction in trace_refute.

I suspect that a lot of time is wasted in loop_bounds on this.

Summarised version of graph output.

Avoids long strings of Basics and assertions (Conds with Err output),
making the overall graph quite readable.

First steps toward floating point support.

This gets mostly just passed through to the relevant SMT logics. Since they're
still transitionally supported it's not clear whether to change the QF_ABV
logic or not.

minor edits

Performance tweaks.

Bugfix.

Defer some analysis during inline phase.

The WCET analysis is keeping us waiting on this a lot.

Port inline workaround from WCET branch.

This leads to less Aborts and more results. It's a bit of a hack
though, but then so was the hardcoded 'C' tag.

More loop search bugfixes.

Make sure report-mode produces output in each case.

Import of graph-refine tool.