package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

Innovation. Community. Security.