sig
type env
type label
type value =
Term
| Addr of Wp.Sigs.s_lval
| Lval of Wp.Sigs.s_lval * Wp.Pcfg.label
| Chunk of string * Wp.Pcfg.label
val create : unit -> Wp.Pcfg.env
val register : Wp.Conditions.sequence -> Wp.Pcfg.env
val at : Wp.Pcfg.env -> id:int -> Wp.Pcfg.label
val find : Wp.Pcfg.env -> Wp.Lang.F.term -> Wp.Pcfg.value
val updates :
Wp.Pcfg.env ->
Wp.Pcfg.label Wp.Sigs.sequence ->
Wp.Lang.F.Vars.t -> Wp.Sigs.update Bag.t
val visible : Wp.Pcfg.label -> bool
val subterms :
Wp.Pcfg.env -> (Wp.Lang.F.term -> unit) -> Wp.Lang.F.term -> bool
val prev : Wp.Pcfg.label -> Wp.Pcfg.label list
val next : Wp.Pcfg.label -> Wp.Pcfg.label list
val iter :
(Wp.Sigs.mval -> Wp.Lang.F.term -> unit) -> Wp.Pcfg.label -> unit
val branching : Wp.Pcfg.label -> bool
class virtual engine :
object
method is_atomic_lv : Wp.Sigs.s_lval -> bool
method pp_addr : Format.formatter -> Wp.Sigs.s_lval -> unit
method virtual pp_atom : Format.formatter -> Wp.Lang.F.term -> unit
method pp_chunk : Format.formatter -> string -> unit
method virtual pp_flow : Format.formatter -> Wp.Lang.F.term -> unit
method pp_host : Format.formatter -> Wp.Sigs.s_host -> unit
method pp_label : Format.formatter -> Wp.Pcfg.label -> unit
method pp_lval : Format.formatter -> Wp.Sigs.s_lval -> unit
method pp_offset : Format.formatter -> Wp.Sigs.s_offset list -> unit
method pp_ofs : Format.formatter -> Wp.Sigs.s_offset -> unit
end
end