sig
val must_translate : Property.t -> bool
val must_translate_opt : Property.t option -> bool
val pre_funspec :
Cil_types.kernel_function ->
Cil_types.kinstr -> Env.t -> Cil_types.funspec -> Env.t
val post_funspec :
Cil_types.kernel_function -> Cil_types.kinstr -> 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