Module Translate_ats

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