sig
val predicate_to_exp :
?name:string ->
Cil_types.kernel_function ->
?rte:bool -> Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t
val generalized_untyped_predicate_to_exp :
?name:string ->
Cil_types.kernel_function ->
?rte:bool ->
?must_clear_typing:bool ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t
val translate_predicate :
?pred_to_print:Cil_types.predicate ->
Cil_types.kernel_function ->
Env.t -> Cil_types.toplevel_predicate -> Env.t
val translate_rte_annots :
(Stdlib.Format.formatter -> 'a -> unit) ->
'a ->
Cil_types.kernel_function ->
Env.t -> Cil_types.code_annotation list -> 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