module Per_stmt_slevel:sig
..end
//@ slevel
directives.type
slevel =
| |
Global of |
(* |
Same slevel i in the entire function
| *) |
| |
PerStmt of |
(* |
Different slevel for different statements
| *) |
val local : Cil_types.kernel_function -> slevel
type
merge =
| |
NoMerge |
(* |
Propagate states according to slevel in the entire function.
| *) |
| |
Merge of |
(* |
Statements on which multiple states should be
merged (instead of being propagated separately)
| *) |
val merge : Cil_types.kernel_function -> merge