E_ACSL.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
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