package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Generate C implementations of E-ACSL \at() terms and predicates.

Translate all \at() predicates and terms for the given statement in the current environment.

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