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