module Translate_ats:sig
..end
Generate C implementations of E-ACSL \at()
terms and predicates.
Generate C implementations of E-ACSL \at()
terms and predicates.
val for_stmt : Env.t -> Cil_types.kernel_function -> Cil_types.stmt -> Env.t
Translate all \at()
predicates and terms for the given statement in the
current environment.
val to_exp : loc:Cil_types.location ->
adata:Assert.t ->
Cil_types.kernel_function ->
Env.t ->
Analyses_types.pred_or_term ->
Cil_types.logic_label -> Cil_types.exp * Assert.t * Env.t
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 ->
Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref
val predicate_to_exp_ref : (adata:Assert.t ->
?inplace:bool ->
?name:string ->
Cil_types.kernel_function ->
?rte:bool ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref