Frama-C API - Translate_terms
Generate C implementations of E-ACSL terms.
val to_exp : adata:Assert.t -> ?inplace:bool -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.exp * Assert.t * Env.tto_exp ~adata ?inplace kf env t converts an ACSL term into a corresponding C expression.
adata: assertion context.inplace: if the root term has a label, indicates if it should be immediately translated or ifTranslate_atsshould be used to retrieve the translation.kf: The enclosing function.env: The current environment.t: The term to translate.
exception No_simple_translation of Frama_c_kernel.Cil_types.termExceptin raised if untyped_to_exp would generate new statements in the environment
val untyped_to_exp : Frama_c_kernel.Cil_types.typ option -> Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.expConvert an untyped ACSL term into a corresponding C expression.
val translate_rte_exp_ref : (?filter:(Frama_c_kernel.Cil_types.code_annotation -> bool) -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Frama_c_kernel.Cil_types.exp -> Env.t) Stdlib.ref