convert license headers to SPDX

Tweaks of the coverage formatting.

Format a coverage report.

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

Bugfixes, loop mode now roughly working.

First attempt: some loop cases in trace_refute.

Tweak to stack availability in trace_refute.

Includes a hack that allows a user to hide a problematic function.

Factor out parent context limit in trace_refute.

Bugfix in trace_refute.

Bug fixes

Bugfixes

Improve loop_bounds induction; avoid nesteds.

New code for making sure loop_bounds avoids nested loops.

Also, a substantial upgrade to how quickly the inductive search package
discovers the true set of inductive invariants.

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.

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.

Bugfix

Note function limits in trace_refute also.

Function limits of zero are a decent way of forbidding access to part of the
system for experimental reasons.

Bugfix.

Bugfix: ensure skip_underspec is passed in prev.

When replacing trace_refute's implementation with check.build_problem, I failed
to note that trace_refute passes a special skip_underspec argument. Fixed.

Faster problem (re-)construction in trace_refute.

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

Hacky parallelisation of trace_refute.py.

Edit for new instruction format in trace_refute.

Split load_target and load_target_args.

fixed typo

Lost updates to trace_refute.

We discovered some more trace_refute work sitting in an old branch.
Merge that into mainline.

Robustness adjustments.

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.

Minor bugfix.

Capture un-paired functions in some analyses.

Functions callable from functions tagged 'ASM' should be analysed
in ASM analysis phases also. Tongue twist that.

More bugfixing and diagnostics for loop_bounds.

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.

Import of graph-refine tool.