Module Translate_ats

module Translate_ats: sig .. end

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

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