module Per_stmt_slevel:sig
..end
module G:sig
..end
module Dfs:Graph.Traverse.Dfs
(
G
)
val retrieve_annot : Cil_types.identified_predicate list -> int option
type
slevel =
| |
Global of |
(* |
Same slevel i in the entire function
| *) |
| |
PerStmt of |
(* |
Different slevel for different statements
| *) |
module DatatypeSlevel:Datatype.Make
(
sig
include Datatype.Undefinedtypet =
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