package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
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