Tweak final report some more.

If we check specific functions, the coverage report is now correct,
rather than erroneously suggesting that everything not even considered
was covered.

Clarify return codes somewhat more.

Aborts are a skip case, not a failure case. Clarify the categories
and make sure that a zero return result occurs in all non-failure
categories.

Set final return value to success more often.

The final process return value is now 0 unless a problem actually
failed. All kinds of underspecified and/or skipped problems are
mapped to 0, so are considered to have succeeded in the 'make'
sense.

Tweaks of the coverage formatting.

Format a coverage report.

This is probably the most useful way to report on which problems
can be built.

Add a mode to just report on coverage.

Builds the problem pairings, but doesn't try to solve any of them.

This is fairly quick, and the report clarifies what we expect the
coverage of the tool to be.

Option to produce a coverage report of sorts.

This skips all the actual proofs and just produces output about why
proofs must be skipped at the problem construction phase.

Use stats scan to skip proofs on partial rebuild.

It's a bit sad, but we need this hack to meet a deadline.

Quick add-on to extract rerun set from result list.

Code for running a subset of problems.

e.g. to split the problems from a target 10 ways:
graph-refine [target] div:0:10
graph-refine [target] div:1:10
..
graph-refine [target] div:9:10

Miniscule tweak to timing.

Better timing messages, especially with psutil.

Bugfix.

Produce a summary for command-line checks.

Tweaks to output and Makefile ignore set.

The decompiler needs to ignore some noreturn functions which don't
reset the stack correctly. Newer seL4 has several more of these.

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.

Bugfixes, also report times in reports.

Minor fixes.

Slight fix at toplevel.

Steps towards testing in l4v regression.

Split load_target and load_target_args.

Support and fixes for loop_bounds.

Fix some atrophied code in trace_refute and make it easier for
standalone scripts (loop_bounds/trace_refute) to load a target.

Improve documentation and output.

Always provide a summary.

New toplevel result for solver timeout/error.

Until now we've been conflating proof failure caused by solver failure
and proof failure caused by logical incorrectness (sat when unsat was
required). Hopefully clarified.

Make sure report-mode produces output in each case.

Make report mode the default.

New 'verbose' restores the previous default, and it will be restored for
interactive checks in any case.

Fix report-to, add progress counts.

Default output of the seL4-example should be much more explicable.

Import of graph-refine tool.