Add additional abort conditions

[danmatichuk]

In #125 we added the ability to prove that an equivalence condition is "valid" in the sense that non-equivalent branches result in the original binary aborting.

Currently an "abort" is defined by a magic function that simply indicates early program termination, but we can extend this to include additional abort conditions. An obvious condition would be a null pointer dereference.