The various assertions which just enforce that the machine's control
flow predicates are consistent with the CFG structure are a bit
pointless.  Get rid of them.
Minor optimisation: if an expression is an address then that can
sometimes rule out some possible leaves, and hence make some internal
tests redundant.  Take advantage of that.
Extract a correct backtrace when we need to go across more than one
function.
Tweak the BDD normaliser so that we don't have bits which assert
BadPtr(x) and then immediately test LD(x).
Another tweak to BDD normalisation: make use of the fact that 0 == K
implies BadPtr(K).
Add a little debug crud to enumEvalPaths.
Kill off dead paths a little bit earlier during symbolic execution.
Turn down enumEvalPaths debug crud a little.
Redo symbolic exection so that it handles assertions (etc) by just
adding the asserted value to the path constraint, rather than creating
a whole new eval context for the case where we fail.
Rework the symbolic execution engine so that it defers aliasing
decisions for as long as possible by pushing them into the load result
exprbdd.
The atomic field of an EvalCtxt is only used for debugging.  Remove
it.
We only ever symbolically execute one state machine at a time, so
there's no point trying to track which machine each store came from.
Make sure we use the specialised address when symbolically executing
loads, rather than the unspecialised one.
Fix a compiler warning.
Try a bit harder to remove all <unreached> state from a cross-product
machine before symbolically executing it.
Tweak the symbolic executor so that it only tracks the assignment
order if there are still Phis present in the machine.
When building a cross product machine it's better to get ``linear''
states out of the way before issuign any bifurcates, because anything
issued after a bifurcate ends up being duplicated unnecessarily.
Bloody stupid hack to make the current test case work without needing
to parse up lots of ELF metadata.
Much better handling of the uninitialised values which can sometimes
creep in.  Basically, we allow the use of uninitialised values
provided it's in the context of a BDD which ensures that the value
never matters.  If the other simpifications can show that a condition
is always true or false then those guards can end up getting removed,
which then indicates that a particular configuration is unreachable.
Make sure that the symbolic executor recognises that and does
something sensible.
Add a mechanism for printing BDDs to DOT files, because that makes it
a bit easier to see their structure.