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