Module Per_stmt_slevel

module Per_stmt_slevel: sig .. end
Fine-tuning for slevel, according to //@ slevel directives.

type slevel = 
| Global of int (*
Same slevel i in the entire function
*)
| PerStmt of (Cil_types.stmt -> int) (*
Different slevel for different statements
*)
val local : Cil_types.kernel_function -> slevel
Slevel to use in this function
type merge = 
| NoMerge (*
Propagate states according to slevel in the entire function.
*)
| Merge of (Cil_types.stmt -> bool) (*
Statements on which multiple states should be merged (instead of being propagated separately)
*)
val merge : Cil_types.kernel_function -> merge
Slevel merge strategy for this function