sig
val translate_pre_spec :
Cil_types.kernel_function ->
Cil_types.kinstr -> Env.t -> Cil_types.funspec -> Env.t
val translate_post_spec :
Cil_types.kernel_function ->
Cil_types.kinstr -> Env.t -> Cil_types.funspec -> Env.t
val translate_pre_code_annotation :
Cil_types.kernel_function ->
Cil_types.stmt -> Env.t -> Cil_types.code_annotation -> Env.t
val translate_post_code_annotation :
Cil_types.kernel_function ->
Cil_types.stmt -> Env.t -> Cil_types.code_annotation -> Env.t
val translate_named_predicate :
Cil_types.kernel_function -> Env.t -> Cil_types.predicate -> Env.t
val translate_rte_annots :
(Format.formatter -> 'a -> unit) ->
'a ->
Cil_types.kernel_function ->
Env.t -> Cil_types.code_annotation list -> Env.t
exception No_simple_translation of Cil_types.term
val term_to_exp : Cil_types.typ option -> Cil_types.term -> Cil_types.exp
val predicate_to_exp :
Cil_types.kernel_function -> Cil_types.predicate -> Cil_types.exp
val set_original_project : Project.t -> unit
end