Frama-C API - `Translate_ats`

Generate C implementations of E-ACSL \at() terms and predicates.

val for_stmt : Env.t -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Env.t

Translate all \at() predicates and terms for the given statement in the current environment.

val to_exp : loc:Frama_c_kernel.Cil_types.location -> adata:Assert.t -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Analyses_types.pred_or_term -> Frama_c_kernel.Cil_types.logic_label -> Frama_c_kernel.Cil_types.exp * Assert.t * Env.t

returns
the C expression corresponding to the given pred_or_term.
The expression is either translated in-place or retrieved from a pre-translation phase.

val reset : unit -> unit

Clear the stored translations.

module Malloc : sig ... end

module Free : sig ... end

val term_to_exp_ref : (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.t) Stdlib.ref

val predicate_to_exp_ref : (adata:Assert.t -> ?inplace:bool -> ?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.t) Stdlib.ref

Frama-C API - Translate_ats

Frama-C API - `Translate_ats`