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.