Frama-C:
Plug-ins:
Libraries:

Frama-C API - P

include JOIN_SEMILATTICE
type t
val join : t -> t -> t

Must be idempotent (join a a = a), commutative, and associative.

val bottom : t

Must verify that forall a, join a bottom = a.

val is_included : t -> t -> bool

Must verify: a is_included b <=> a join b = b. The dataflow does not require this function.

val join_and_is_included : t -> t -> t * bool

This function is used by the dataflow algorithm to determine if something has to be recomputed. Joining and inclusion testing are similar operations, so it is often more efficient to do both at the same time (e.g. when joining with bottom).

Instead of defining it directly, it can be defined from join and equal, or from is_included, for instance by if is_included new old then (true,old) else (false, join old new) or let j = join old new in (equal j new, j).

val pretty : Stdlib.Format.formatter -> t -> unit

Display the contents of an element of the lattice.

val transfer_stmt : Cil_types.stmt -> t -> (Cil_types.stmt * t) list

transfer_stmt s state must returns a list of pairs in which the first element is a statement s' in s.succs, and the second element a value that will be joined with the current result for before s'.

Note that it is allowed that not all succs are present in the list returned by transfer_stmt (in which case, the successor is assumed to be unreachable in the current state), or that succs are present several times (this is useful to handle switches).

Helper functions are provided for If and Switch statements. See transfer_if_from_guard and transfer_switch_from_guard below.

val init : (Cil_types.stmt * t) list

The initial value for each statement. Statements in this list are given the associated value, and are added to the worklist. Other statements are initialized to bottom.

Unless you want to do something very specific, supplying only the state for the first statement of the function (as found by Kernel_function.find_first_stmt) is sufficient.