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

type env

type label

type value =

| Term

| Addr of Sigs.s_lval

| Lval of Sigs.s_lval * label

| Init of Sigs.s_lval * label

| Chunk of string * label

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 Sigs.sequence ->
  Lang.F.Vars.t ->
  Sigs.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 : ( Sigs.mval -> Lang.F.term -> unit ) -> label -> unit

val branching : label -> bool

class virtual engine : object ... end