Frama-C:
Plug-ins:
Libraries:

Frama-C API - Pcfg

type env
type label
type value =
  1. | Term
  2. | Addr of Memory.s_lval
  3. | Lval of Memory.s_lval * label
  4. | Init of Memory.s_lval * label
  5. | Chunk of Sigma.chunk * label
val create : unit -> env
val register : Conditions.sequence -> env
val at : env -> id:int -> label
val find : env -> Lang.F.term -> value
val visible : label -> bool
val subterms : env -> (Lang.F.term -> unit) -> Lang.F.term -> bool
val prev : label -> label list
val next : label -> label list
val iter : (Memory.mval -> Lang.F.term -> unit) -> label -> unit
val branching : label -> bool
class virtual engine : object ... end