Module Prepare_ast

module Prepare_ast: sig .. end

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 -> 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 : (Cil_types.varinfo -> bool) Stdlib.ref