Frama-C:
Plug-ins:
Libraries:

Frama-C API - Traces_domain

Traces domain

module GraphShape : sig ... end
type node = Node.t
and edge = {
  1. edge_trans : transition;
  2. edge_dst : node;
}
module Edge : Frama_c_kernel.Datatype.S with type t = edge
module Graph : sig ... end
type loops =
  1. | Base of Node.t * Graph.t
  2. | OpenLoop of Frama_c_kernel.Cil_types.stmt * Node.t * Graph.t * Node.t * Graph.t * loops
    (*

    OpenLoop(stmt, starting_node, last_iteration, current_node, g, loop)

    *)
  3. | UnrollLoop of Frama_c_kernel.Cil_types.stmt * loops

stack of open loops

module Loops : sig ... end
type state
val start : state -> Node.t
val current : state -> loops
val entry_formals : state -> Frama_c_kernel.Cil_types.varinfo list