convert license headers to SPDX

Always flush on printout()

Some flushing was done during proof checking, but it might as well
be unconditional on printout() messages.

Experiment with side-proving rodata ineqs.

The suspicion was that some slow-down seen lately was because the
rodata-witness value might now have a disjunction of possible
reasons for difference, which might make the solver logic for
understanding that function input are valid more obscure. A possible
fix for that is to pre-test and pre-assert that the witness must be
disjoint from problem pointers on the C side, based just on their PC.
That should simplify the SMT logic, one might think.

Tweak to stack availability in trace_refute.

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

Fix previous; include a compatibility workaround.

Fixes a bug in previous.

Also adds a hook whereby a target can request a previous level of
compatibility with functions that contain ASM statements and other
non-calling-convention compatible functions that may dangerously
adjust the stack pointer.

(The previous level of compatibility is actually unsound, because
it assumed that e.g. the fastpath restore assembly block did not
do what it did.)

loop_bounds: more principle for preemptionPoint

We've been manually adding bounds for functions which call preemptionPoint, but
that means manually checking that we've found them all, and for larger numbers
of runs I'm starting to make mistakes. Add a mechanism to quickly check this.
Has to be configured to the name of the functions limited. Also allows pruning
functions considered unreachable in this run.

Bugfix again.

Turns out __package__ is unreliable, let's just use the prefix
of __name__.

Fix previous.

Split load_target and load_target_args.

Make target_objects.load_target work with packages.

Add arg-override to target_objects.load_target ()

Further bugfixes for linked problems.

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.