Module Traces_domain

module Traces_domain: sig .. end
Traces domain

traces domain


module Node: Datatype.S 
module GraphShape: sig .. end
Can't use Graph.t it needs an impossible recursive module
type node = Node.t 
type transition = 
| Assign of Cil_types.kinstr * Cil_types.lval * Cil_types.typ * Cil_types.exp
| Assume of Cil_types.stmt * Cil_types.exp * bool
| EnterScope of Cil_types.kernel_function * Cil_types.varinfo list
| LeaveScope of Cil_types.kernel_function * Cil_types.varinfo list (*
For call of functions without definition

For call of functions without definition

*)
| CallDeclared of Cil_types.kernel_function * Cil_types.exp list * Cil_types.lval option
| Loop of Cil_types.stmt * node
* edge list GraphShape.t
| Msg of string
type edge = {
   edge_trans : transition;
   edge_dst : node;
}
module Edge: Datatype.S  with type t = edge
module Graph: sig .. end
type loops = 
| Base of Node.t * Graph.t
| OpenLoop of Cil_types.stmt * Node.t * Graph.t * Node.t
* Graph.t * loops
| UnrollLoop of Cil_types.stmt * loops
stack of open loops
module Loops: sig .. end
type state 
val start : state -> Node.t
val current : state -> loops
val globals : state -> Cil_types.varinfo list
val entry_formals : state -> Cil_types.varinfo list
module D: Abstract_domain.Leaf 
  with type value = Cvalue.V.t
   and type location = Precise_locs.precise_location
   and type state = state