Module Frama_c_kernel.State_dependency_graph

State Dependency Graph.

Signatures

module type S = sig ... end

Signature of a State Dependency Graph. It is compatible with the signature of OcamlGraph imperative graph Graph.Sig.I.

module type Attributes = sig ... end

Signature required by Graph.GraphViZ.Dot. See the OcamlGraph's documentation for additional details.

include S
module G : Graph.Sig.G with type V.t = State.t and type E.t = State.t * State.t
val graph : G.t
val add_dependencies : from:State.t -> State.t list -> unit

Add an edge in graph from the state from to each state of the list.

  • since Carbon-20101201
val add_codependencies : onto:State.t -> State.t list -> unit

Add an edge in graph from each state of the list to the state onto.

  • since Carbon-20101201
val remove_dependencies : from:State.t -> State.t list -> unit

Remove an edge in graph from the given state to each state of the list.

  • since Fluorine-20130401
val remove_codependencies : onto:State.t -> State.t list -> unit

Remove an edge in graph from each state of the list to the state onto.

  • since Oxygen-20120901
val add_state : State.t -> State.t list -> unit
module Dot (_ : Attributes) : sig ... end
val dump : string -> unit