Module Per_stmt_slevel

module Per_stmt_slevel: sig .. end
Same slevel i in the entire function

module G: sig .. end
module Dfs: Graph.Traverse.Dfs(G)
val retrieve_annot : Cil_types.identified_predicate list -> int option
type slevel = 
| Global of int (*
Same slevel i in the entire function
*)
| PerStmt of (Cil_types.stmt -> int) (*
Different slevel for different statements
*)
module DatatypeSlevel: Datatype.Make(sig
include Datatype.Undefined
type t = Per_stmt_slevel.slevel 
val reprs : Per_stmt_slevel.slevel list
val name : string
val mem_project : (Project_skeleton.t -> bool) -> 'a -> bool
end)
val extract_slevel_directive : Cil_types.stmt -> int option option
val kf_contains_slevel_directive : Kernel_function.t -> bool
val for_kf : ForKf.key -> ForKf.data
module ForKf: Kernel_function.Make_Table(DatatypeSlevel)(sig
val size : int
val dependencies : State.t list
val name : string
end)
val for_kf : ForKf.key -> ForKf.data