state (frama-c-wp.Wp.Pcond.state)

inherit Wp__.Plang.engine

inherit Wp__.Pcfg.engine

method clear : unit

method set_sequence : Wp__.Conditions.sequence -> unit

method set_domain : Wp__.Lang.F.Vars.t -> unit

Default is sequence's domain

method domain : Wp__.Lang.F.Vars.t

method label_at : id:int -> Wp__.Pcfg.label

method updates : Wp__.Pcfg.label Wp__.Sigs.sequence ->
  Wp__.Sigs.update Frama_c_kernel.Bag.t

method pp_at : Stdlib.Format.formatter -> Wp__.Pcfg.label -> unit

method pp_update : Wp__.Pcfg.label ->
  Stdlib.Format.formatter ->
  Wp__.Sigs.update ->
  unit

method pp_value : Stdlib.Format.formatter -> Wp__.Lang.F.term -> unit