sig
val apply_after_transformation : Project.t -> unit
val mv_invariants : Env.t -> old:Cil_types.stmt -> Cil_types.stmt -> unit
val preserve_invariant :
Project.t ->
Env.t ->
Kernel_function.t -> Cil_types.stmt -> Cil_types.stmt * Env.t * bool
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_named_predicate_ref :
(Cil_types.kernel_function -> Env.t -> Cil_types.predicate -> Env.t)
Stdlib.ref
val named_predicate_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