Module `Goblint_lib.CfgTools`

Construction and output of CFGs.

module H = MyCFG.NodeH

module NH = MyCFG.NodeH

val find_backwards_reachable : 
  initial_size:int ->
  (module MyCFG.CfgBackward) ->
  MyCFG.node ->
  unit NH.t

module SCC : sig ... end

Strongly connected component.

val computeSCCs : 
  (module MyCFG.CfgBidir) ->
  NH.key list ->
  SCC.t list * SCC.t NH.t

val pretty_edges : unit -> ('a * Edge.t) list -> GoblintCil.Pretty.doc

val get_pseudo_return_id : GoblintCil.fundec -> int

val node_scc_global : SCC.t NH.t

exception Not_connect of GoblintCil.fundec

module CfgEdge : sig ... end

Type of CFG "edges": keyed by 'from' and 'to' nodes, along with the list of connecting instructions.

module CfgEdgeH : sig ... end

val createCFG : 
  GoblintCil.file ->
  (MyCFG.edges * Node.t) list H.t
  * (MyCFG.edges * Node.t) list H.t
  * CilType.Stmt.t list CfgEdgeH.t

val minimizeCFG : 
  ('a list H.t * (MyCFG.edges * Node.t) list H.t) ->
  CilType.Stmt.t list CfgEdgeH.t ->
  ((CilType.Location.t * Edge.t) list * H.key) list H.t
  * ((CilType.Location.t * Edge.t) list * H.key) list H.t
  * CilType.Stmt.t list CfgEdgeH.t

module type CfgPrinters = sig ... end

module type NodeStyles = sig ... end

module CfgPrinters (NodeStyles : NodeStyles) : sig ... end

val fprint_dot : 
  (module CfgPrinters) ->
  ((MyCFG.node ->
     ((GoblintCil.location * MyCFG.edge) list * MyCFG.node) ->
     unit) ->
    'a) ->
  Format.formatter ->
  unit

val fprint_hash_dot : 
  ((GoblintCil.location * MyCFG.edge) list * MyCFG.node) list H.t ->
  unit

val getCFG : 
  GoblintCil.file ->
  MyCFG.cfg * MyCFG.cfg * GoblintCil.stmt list CfgEdgeH.t

val iter_fd_edges : 
  (module MyCFG.CfgBackward) ->
  CilType.Fundec.t ->
  (MyCFG.node -> ((CilType.Location.t * Edge.t) list * Node.t) -> unit) ->
  unit

val fprint_fundec_html_dot : 
  (module MyCFG.CfgBidir) ->
  (MyCFG.node -> bool) ->
  CilType.Fundec.t ->
  Format.formatter ->
  unit

val sprint_fundec_html_dot : 
  (module MyCFG.CfgBidir) ->
  (MyCFG.node -> bool) ->
  CilType.Fundec.t ->
  string

val dead_code_cfg : (module MyCFG.FileCfg) -> (MyCFG.node -> bool) -> unit

val getGlobalInits : GoblintCil.file -> MyCFG.edges

val numGlobals : GoblintCil.Cil.file -> int

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/CfgTools/index.html

Module `Goblint_lib.CfgTools`

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblint_lib/CfgTools/index.html

Module Goblint_lib.CfgTools

Module `Goblint_lib.CfgTools`