Frama-C API - Translate_predicates
Generate C implementations of E-ACSL predicates.
val generalized_untyped_to_exp : adata:Assert.t -> ?name:string -> Frama_c_kernel.Cil_types.kernel_function -> ?rte:bool -> Env.t -> Frama_c_kernel.Cil_types.predicate -> Frama_c_kernel.Cil_types.exp * Assert.t * Env.tConvert an untyped ACSL predicate into a corresponding C expression.
val do_it : ?pred_to_print:Frama_c_kernel.Cil_types.predicate -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Frama_c_kernel.Cil_types.toplevel_predicate -> Env.tTranslate the given predicate to a runtime check in the given environment. If pred_to_print is set, then the runtime check will use this predicate as message.
exception No_simple_translation of Frama_c_kernel.Cil_types.predicateExceptin raised if untyped_to_exp would generate new statements in the environment
val untyped_to_exp : Frama_c_kernel.Cil_types.predicate -> Frama_c_kernel.Cil_types.expConvert an untyped ACSL predicate into a corresponding C expression. This expression is valid only in certain contexts and shouldn't be used.
val translate_rte_annots_ref : ((Stdlib.Format.formatter -> Frama_c_kernel.Cil_types.code_annotation -> unit) -> Frama_c_kernel.Cil_types.code_annotation -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Frama_c_kernel.Cil_types.code_annotation list -> Env.t) Stdlib.refval 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