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
typenode =
Node.t
type
transition =
| |
Assign of |
|||
| |
Assume of |
|||
| |
EnterScope of |
|||
| |
LeaveScope of |
(* | For call of functions without definition For call of functions without definition | *) |
| |
CallDeclared of |
|||
| |
Loop of |
|||
| |
Msg of |
type
edge = {
|
edge_trans : |
|
edge_dst : |
module Edge:Datatype.S
with type t = edge
module Graph:sig
..end
type
loops =
| |
Base of |
| |
OpenLoop of |
| |
UnrollLoop of |
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