sig
val handle_annotations :
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.toplevel_predicate -> Env.t)
Stdlib.ref
val predicate_to_exp_ref :
(adata:Assert.t ->
Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref
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
end