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

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

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/frama-c-e-acsl.core/E_ACSL/Translate_ats/index.html

Module `E_ACSL.Translate_ats`

package frama-c

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/frama-c-e-acsl.core/E_ACSL/Translate_ats/index.html

Module E_ACSL.Translate_ats

dune-project
Dependency

Module `E_ACSL.Translate_ats`