Frama-C:
Plug-ins:
Libraries:

Frama-C API - Mark

Signature of the module to use in order to instantiate the computation

type t

type of the information mapped to the nodes

type call_info

type of the information mapped to the function calls. This can be unit if there is nothing to store for the calls. (see PdgIndex.FctIndex for more information)

val is_bottom : t -> bool

used to test combine result (see below)

val merge : t -> t -> t

merge two pieces of information

val combine : t -> t -> t * t

combine is used during propagation. It should return (new_mark, mark_to_prop) = combine old_mak new_mark where new_mark is the mark to associate with the node, and mark_to_prop the mark to propagate to its dependencies. If is_bottom mark_to_prop, the propagation is stopped.

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