module Per_stmt_slevel:sig
..end
Fine-tuning for slevel, according to //@ 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
Slevel to use in this function
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
Slevel merge strategy for this function