Frama-C API - Per_stmt_slevel
Fine-tuning for slevel, according to //@ slevel directives.
type slevel = | Global of int(*Same slevel i in the entire function
*)| PerStmt of Frama_c_kernel.Cil_types.stmt -> int(*Different slevel for different statements
*)
val local : Frama_c_kernel.Cil_types.kernel_function -> slevelSlevel to use in this function
type merge = | NoMerge(*Propagate states according to slevel in the entire function.
*)| Merge of Frama_c_kernel.Cil_types.stmt -> bool(*Statements on which multiple states should be merged (instead of being propagated separately)
*)
val merge : Frama_c_kernel.Cil_types.kernel_function -> mergeSlevel merge strategy for this function