Pcfg (frama-c-wp.Wp.Pcfg)

type env

type label

type value =

val create : unit -> env

val register : Conditions.sequence -> env

val at : env -> id:int -> label

val find : env -> Lang.F.term -> value

val updates : 
  env ->
  label Memory.sequence ->
  Lang.F.Vars.t ->
  Memory.update Frama_c_kernel.Bag.t

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