Module Mcfg

module Mcfg: sig .. end
This is what is really needed to propagate something through the CFG. Usually, the propagated thing should be a predicate, but it can be more sophisticated like lists of predicates, or maybe a structure to keep hypotheses and goals separated. Moreover, proof obligations may also need to be handeled.

type scope = 
| SC_Global
| SC_Function_in
| SC_Function_frame
| SC_Function_out
| SC_Block_in
| SC_Block_out
module type Export = sig .. end
module type Splitter = sig .. end
module type S = sig .. end
This is what is really needed to propagate something through the CFG.