Frama-C API - `Prepare_ast`

Prepare AST for E-ACSL generation.

More precisely, this module performs the following tasks:

generating a new definition for functions with contract;
removing term sharing;
in case of temporal validity checks, adding the attribute "aligned" to variables that are not sufficiently aligned;
create a block around a labeled statement to hold the labels so that the code generation does not need to change the statement holding the label.

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

Frama-C API - Prepare_ast