package binsec

  1. Overview
  2. Docs
Semantic analysis of binary executables

Install 

dune-project
 Dependency

binsec.github.io Readme Changelog LGPL-2.1-or-later License Edit opam file Versions (18)

Authors

  1. A
    Adel Djoudi
  2. B
    Benjamin Farinier
  3. C
    Chakib Foulani
  4. D
    Dorian Lesbre
  5. F
    Frédéric Recoules
  6. G
    Guillaume Girol
  7. J
    Josselin Feist
  8. L
    Lesly-Ann Daniel
  9. M
    Manh-Dung Nguyen
  10. M
    Mathéo Vergnolle
  11. M
    Mathilde Ollivier
  12. M
    Matthieu Lemerre
  13. O
    Olivier Nicole
  14. R
    Richard Bonichon
  15. R
    Robin David
  16. S
    Sébastien Bardin
  17. S
    Soline Ducousso
  18. T
    Ta Thanh Dinh
  19. Y
    Yaëlle Vinçont

Maintainers

  1. B
    BINSEC <binsec@saxifrage.saclay.cea.fr>

Sources

binsec-0.7.2.tbz
sha256=5e1d0f26a567df4abcbeb964b454cf8b2c8484194ff2d9639bdeb94d63edcb3b
sha512=a638c665407fde9aadbd57a7b9f84260db8f03c0cbf65722732d43dfc93122d801e31977e0ba7cd249b340262caf216bca746a3520d0e01d487a5baf6a6c77e6

doc/binsec/Binsec/Cfg/Make/index.html

Module Cfg.Make

Parameters

module A : Sigs.HASHABLE

Signature

type addr = A.t
type inst = I.t
type symb = S.t
type t

Abstract type of graphs

module V : sig ... end

Vertices

type vertex = V.t
module E : sig ... end

Edges

type edge = E.t
module Fixpoint (X : sig ... end) : sig ... end
type trace = vertex Sequence.t
val is_directed : bool

is this an implementation of directed graphs?

Graph constructors and destructors

val create : int -> t

Return an empty graph. Optionally, a size can be given, which should be on * the order of the expected number of vertices that will be in the graph (for * hash tables-based implementations). The graph grows as needed, so size is * just an initial guess.

val clear : t -> unit

Remove all vertices and edges from the given graph.

val copy : t -> t

copy g returns a copy of g. Vertices and edges (and eventually marks, * see module Mark) are duplicated.

val add_vertex : t -> vertex -> unit

add_vertex g v adds the vertex v in graph g. Do nothing if v * is already in g.

val add_addr : t -> addr -> unit
val add_inst : t -> addr -> inst -> unit
val add_symb : t -> addr -> symb -> unit
val remove_vertex : t -> vertex -> unit

remove g v removes the vertex v from the graph g (and all the edges * going from v in g). Do nothing if v is not in g.

val remove_addr : t -> addr -> unit
val remove_inst : t -> addr -> unit
val remove_symb : t -> addr -> unit
val add_edge : t -> vertex -> vertex -> unit

add_edge g v1 v2 adds an edge from the vertex v1 to the vertex v2 in * the graph g. Add also v1 (resp. v2) in g if v1 (resp. v2) is not * in g. Do nothing if this edge is already in g.

val add_edge_a : t -> addr -> addr -> unit
val add_edge_e : t -> edge -> unit

add_edge_e g e adds the edge e in the graph g. Add also E.src e * (resp. E.dst e) in g if E.src e (resp. E.dst e) is not in g. Do * nothing if e is already in g.

val remove_edge : t -> vertex -> vertex -> unit

remove_edge g v1 v2 removes the edge going from v1 to v2 from the * graph g. Do nothing if this edge is not in g. *

val remove_edge_a : t -> addr -> addr -> unit
val remove_edge_e : t -> edge -> unit

remove_edge_e g e removes the edge e from the graph g. Do nothing if * e is not in g. *

Size functions

val is_empty : t -> bool
val nb_vertex : t -> int
val nb_edges : t -> int

Degree of a vertex

val out_degree : t -> vertex -> int

out_degree g v returns the out-degree of v in g. *

val in_degree : t -> vertex -> int

in_degree g v returns the in-degree of v in g. *

Membership functions

val mem_vertex : t -> vertex -> vertex option
val mem_vertex_a : t -> addr -> vertex option
val mem_edge : t -> vertex -> vertex -> edge option
val mem_edge_a : t -> addr -> addr -> edge option
val mem_edge_e : t -> edge -> edge option

Successors and predecessors of a vertex

val succ : t -> vertex -> vertex list

succ g v returns the successors of v in g. *

val pred : t -> vertex -> vertex list

pred g v returns the predecessors of v in g. *

Labeled edges going from/to a vertex

val succ_e : t -> vertex -> edge list

succ_e g v returns the edges going from v in g. *

val pred_e : t -> vertex -> edge list

pred_e g v returns the edges going to v in g. *

Graph iterators

iter/fold on all vertices/edges of a graph

val iter_vertex : (vertex -> unit) -> t -> unit
val iter_edges : (vertex -> vertex -> unit) -> t -> unit
val fold_vertex : (vertex -> 'a -> 'a) -> t -> 'a -> 'a
val fold_edges : (vertex -> vertex -> 'a -> 'a) -> t -> 'a -> 'a

iter/fold on all labeled edges of a graph

val iter_edges_e : (edge -> unit) -> t -> unit
val fold_edges_e : (edge -> 'a -> 'a) -> t -> 'a -> 'a

Vertex iterators

Each iterator iterator f v g iters f to the successors/predecessors of v in the graph g and raises Invalid_argument if v is not in g.

iter/fold on all successors/predecessors of a vertex.

val iter_succ : (vertex -> unit) -> t -> vertex -> unit
val iter_pred : (vertex -> unit) -> t -> vertex -> unit
val fold_succ : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
val fold_pred : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a

iter/fold on all edges going from/to a vertex.

val iter_succ_e : (edge -> unit) -> t -> vertex -> unit
val fold_succ_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
val iter_pred_e : (edge -> unit) -> t -> vertex -> unit
val fold_pred_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a