Forward Constraint System

[michael-schwarz]

This generates an equivalent forward propagating constraint system:

• Uses ForwardCFG with all updates happening via sidel
• Instantiates globals as spec globals plus with auxiliary globals for returns per fundec and context
• In tf_proc use getg to get end state of procedure
• In tf_ret side effect to appropriate helper global

It also presents Helmut's new forward solver.

[michael-schwarz]

This is now a rudimentary version of the solver that works. Missing for something we can use in Goblint are:

• Post-solver like iteration over results to produce warnings (using check) (done)
• Fix detection of uncalled functions (done)
• Extensive testing
• Refactoring to increase reuse between constraints.ml and fwdConstraints.ml
• Refactoring to avoid duplication between control.ml and fwdControl.ml

Plus all further features such as witness generation, SV-COMP verdicts, etc

[michael-schwarz]

Also, we need a new concept of dead code detection, it is no longer the case that we will explicitly compute bot for such nodes.