sig
val preserve_invariant :
Env.t -> Kernel_function.t -> Cil_types.stmt -> Cil_types.stmt * Env.t
val mk_nested_loops :
loc:Cil_types.location ->
(Env.t -> Cil_types.stmt list * Env.t) ->
Cil_types.kernel_function ->
Env.t -> Lscope.lscope_var list -> Cil_types.stmt list * Env.t
val translate_predicate_ref :
(Cil_types.kernel_function -> Env.t -> Cil_types.predicate -> Env.t)
Stdlib.ref
val predicate_to_exp_ref :
(Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t)
Stdlib.ref
val term_to_exp_ref :
(Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Env.t)
Stdlib.ref
end