sig
  val generalized_untyped_to_exp :
    adata:Assert.t ->
    ?name:string ->
    Cil_types.kernel_function ->
    ?rte:bool ->
    Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t
  val do_it :
    ?pred_to_print:Cil_types.predicate ->
    Cil_types.kernel_function ->
    Env.t -> Cil_types.toplevel_predicate -> Env.t
  exception No_simple_translation of Cil_types.predicate
  val untyped_to_exp : Cil_types.predicate -> Cil_types.exp
  val translate_rte_annots_ref :
    ((Stdlib.Format.formatter -> Cil_types.code_annotation -> unit) ->
     Cil_types.code_annotation ->
     Cil_types.kernel_function ->
     Env.t -> Cil_types.code_annotation list -> Env.t)
    Stdlib.ref
  val translate_rte_exp_ref :
    (?filter:(Cil_types.code_annotation -> bool) ->
     Cil_types.kernel_function -> Env.t -> Cil_types.exp -> Env.t)
    Stdlib.ref
end