State_dependency_graph (frama-c.Frama_c_kernel.State_dependency

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 = Frama_c_kernel.State.t
     and type E.t = Frama_c_kernel.State.t * Frama_c_kernel.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.

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.

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.

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.

val add_state : State.t -> State.t list -> unit

module Attributes : Attributes

module Dot (_ : Attributes) : sig ... end

val dump : Filepath.t -> unit