E_ACSL.Translate_atsGenerate 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.tTranslate 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.tThe expression is either translated in-place or retrieved from a pre-translation phase.
module Malloc : sig ... endmodule Free : sig ... endval 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)
refval 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)
ref