Generalize check_pre to handle singe and comparative analysis correctly

[codyroux]

Currently we have combined_pre (

cbat_tools/wp/plugin/lib/wp_analysis.ml

Line 35 in 85dff9a

type combined_pre = {

) as the input type to the check_pre function (and therefore the output of single and comparative.

The problem is that this type assumes both orig and modif fields (env * sub term pairs) exist, which is not always the case.

We should fix this, as it is already causing problems with some branches, and will surely be a source of issues in the future.

My recommendation would be to have a wrapper type type check_res = Single of ?? | Double of ?? which handles both possibilities, and pass that around to check_pre and Output.print_result, which can then operate as needed.

But there are many possible approaches.