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