Module E_ACSL.Prepare_ast

Prepare AST for E-ACSL generation.

More precisely, this module performs the following tasks:

val prepare : unit -> unit

Prepare the AST

val sound_verdict : unit -> Frama_c_kernel.Cil_types.varinfo
  • returns

    the varinfo representing the E-ACSL global variable that indicates whether the verdict emitted by E-ACSL is sound.

val is_libc_writing_memory_ref : ( Frama_c_kernel.Cil_types.varinfo -> bool ) Stdlib.ref