sig
  val translate_pre_spec :
    Cil_types.kernel_function -> Env.t -> Cil_types.funspec -> Env.t
  val translate_post_spec :
    Cil_types.kernel_function -> Env.t -> Cil_types.funspec -> Env.t
  val translate_pre_code_annotation :
    Cil_types.kernel_function -> Env.t -> Cil_types.code_annotation -> Env.t
  val translate_post_code_annotation :
    Cil_types.kernel_function -> Env.t -> Cil_types.code_annotation -> Env.t
  val translate_named_predicate :
    Cil_types.kernel_function -> Env.t -> Cil_types.predicate -> Env.t
  val translate_rte_annots :
    (Format.formatter -> '-> unit) ->
    '->
    Cil_types.kernel_function ->
    Env.t -> Cil_types.code_annotation list -> Env.t
  exception No_simple_translation of Cil_types.term
  val term_to_exp : Cil_types.typ option -> Cil_types.term -> Cil_types.exp
  val predicate_to_exp :
    Cil_types.kernel_function -> Cil_types.predicate -> Cil_types.exp
end