Module Wp.Pcfg

module Pcfg: sig .. end

type env

type label

type value =

`\|`	`Term`
`\|`	`Addr of Wp.Sigs.s_lval`
`\|`	`Lval of Wp.Sigs.s_lval * label`
`\|`	`Init of Wp.Sigs.s_lval * label`
`\|`	`Chunk of string * label`

val create : unit -> env

val register : Wp.Conditions.sequence -> env

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

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

val updates : env ->
       label Wp.Sigs.sequence -> Wp.Lang.F.Vars.t -> Wp.Sigs.update Bag.t

val visible : label -> bool

val subterms : env -> (Wp.Lang.F.term -> unit) -> Wp.Lang.F.term -> bool

val prev : label -> label list

val next : label -> label list

val iter : (Wp.Sigs.mval -> Wp.Lang.F.term -> unit) -> label -> unit

val branching : label -> bool

class virtual engine : object .. end