Frama-C:
Plug-ins:
Libraries:

Frama-C API - UnrollUnnatural

Control flow graphs where unnatural loops are modified such that all paths entering a loop enters it by its head.

include Graph with type V.t = Version.t and type E.t = Version.t * Version.t edge * Version.t and type V.label = Version.t and type E.label = Version.t edge
include Graph.Sig.I with type V.t = Version.t with type E.t = Version.t * Version.t edge * Version.t with type V.label = Version.t with type E.label = Version.t edge
type t
module V : sig ... end
type vertex = V.t
module E : sig ... end
type edge = E.t
val is_directed : bool
val is_empty : t -> bool
val nb_vertex : t -> int
val nb_edges : t -> int
val out_degree : t -> vertex -> int
val in_degree : t -> vertex -> int
val mem_vertex : t -> vertex -> bool
val mem_edge : t -> vertex -> vertex -> bool
val mem_edge_e : t -> edge -> bool
val find_edge : t -> vertex -> vertex -> edge
val find_all_edges : t -> vertex -> vertex -> edge list
val succ : t -> vertex -> vertex list
val pred : t -> vertex -> vertex list
val succ_e : t -> vertex -> edge list
val pred_e : t -> vertex -> edge list
val iter_vertex : (vertex -> unit) -> t -> unit
val fold_vertex : (vertex -> 'a -> 'a) -> t -> 'a -> 'a
val iter_edges : (vertex -> vertex -> unit) -> t -> unit
val fold_edges : (vertex -> vertex -> 'a -> 'a) -> t -> 'a -> 'a
val iter_edges_e : (edge -> unit) -> t -> unit
val fold_edges_e : (edge -> 'a -> 'a) -> t -> 'a -> 'a
val map_vertex : (vertex -> vertex) -> t -> t
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
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
val create : ?size:int -> unit -> t
val clear : t -> unit
val copy : t -> t
val add_vertex : t -> vertex -> unit
val remove_vertex : t -> vertex -> unit
val add_edge : t -> vertex -> vertex -> unit
val add_edge_e : t -> edge -> unit
val remove_edge : t -> vertex -> vertex -> unit
val remove_edge_e : t -> edge -> unit
module VTable : Hashtbl.S with type key = vertex
module WTO : Wto.S with type node = vertex
val build_wto : pref:WTO.pref -> t -> V.t -> wto

Build a wto for the given automaton. The pref function is a comparison function used to determine what is the best vertex to use as a Wto component head. See Wto.Make for more details.

val output_to_dot : ?pp_vertex:V.t Pretty_utils.formatter -> ?pp_edge:E.label Pretty_utils.formatter -> ?wto:wto -> Stdlib.out_channel -> t -> unit

Output the automaton in dot format

val exit_strategy : t -> V.t Wto.component -> wto

Extract an exit strategy from a component, i.e. a sub-wto where all vertices lead outside the wto without passing through the head.

type 'a widening =
  1. | Fixpoint
  2. | Widening of 'a

Widening for abstract domains

module type Domain = sig ... end

Abstract domains

module ForwardAnalysis (D : Domain) : sig ... end

Forward dataflow analysis

module BackwardAnalysis (D : Domain) : sig ... end

Forward dataflow analysis

val build : automaton -> G.vertex Wto.partition -> WTOIndex.Table.t -> t