sig
val must_translate : Property.t -> bool
val must_translate_opt : Property.t option -> bool
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
val comparison_to_exp :
adata:Assert.t ->
loc:Cil_types.location ->
Cil_types.kernel_function ->
Env.t ->
Typing.number_ty ->
?e1:Cil_types.exp ->
Cil_types.binop ->
Cil_types.term ->
Cil_types.term ->
?name:string -> Cil_types.term option -> Cil_types.exp * Assert.t * Env.t
val conditional_to_exp :
?name:string ->
loc:Cil_types.location ->
Cil_types.kernel_function ->
Cil_types.term option ->
Cil_types.exp ->
Cil_types.exp * Env.t -> Cil_types.exp * Env.t -> Cil_types.exp * Env.t
val env_of_li :
adata:Assert.t ->
loc:Cil_types.location ->
Cil_types.kernel_function ->
Env.t -> Cil_types.logic_info -> Assert.t * Env.t
val term_to_exp_ref :
(adata:Assert.t ->
Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref
val predicate_to_exp_ref :
(adata:Assert.t ->
?name:string ->
Cil_types.kernel_function ->
?rte:bool ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref
end