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(siginclude 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