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