sig
  val predicate_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 generalized_untyped_predicate_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 translate_predicate :
    ?pred_to_print:Cil_types.predicate ->
    Cil_types.kernel_function ->
    Env.t -> Cil_types.toplevel_predicate -> Env.t
  val term_to_exp :
    adata:Assert.t ->
    Cil_types.kernel_function ->
    Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t
  val translate_rte_annots :
    (Stdlib.Format.formatter -> '-> unit) ->
    '->
    Cil_types.kernel_function ->
    Env.t -> Cil_types.code_annotation list -> Env.t
  val gmp_to_sizet :
    adata:Assert.t ->
    loc:Cil_types.location ->
    name:string ->
    ?check_lower_bound:bool ->
    ?pp:Cil_types.term ->
    Cil_types.kernel_function ->
    Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t
  exception No_simple_term_translation of Cil_types.term
  exception No_simple_predicate_translation of Cil_types.predicate
  val untyped_term_to_exp :
    Cil_types.typ option -> Cil_types.term -> Cil_types.exp
  val untyped_predicate_to_exp : Cil_types.predicate -> Cil_types.exp
end