Develop an initial way to explain trace differences

[travitch]

The Weakest Precondition solver had differential summaries. This notion doesn't necessarily translate cleanly to the Strongest Postcondition solver. We still need some way to tell users where divergence in traces emerges from. One proposed plan is:

• Record the location (basic block address plus path condition) where each memory divergence is detected in the abstract domain
• When traces diverge, look at the causes of that divergence (e.g., value written to memory mapped IO or argument passed to system call) and look for any explanations that those values depend on

In the future, we can record more information to enable us to re-compute differential summaries