sig
val pre_funspec :
Cil_types.kernel_function -> Env.t -> Cil_types.funspec -> Env.t
val post_funspec : Cil_types.kernel_function -> Env.t -> Env.t
val pre_code_annotation :
Cil_types.kernel_function ->
Cil_types.stmt -> Env.t -> Cil_types.code_annotation -> Env.t
val post_code_annotation :
Cil_types.kernel_function ->
Cil_types.stmt -> Env.t -> Cil_types.code_annotation -> Env.t
end