UpdateRule (p.goblint.2.6.0.doc.goblint.solver.Goblint

Parameters

module S : Goblint_constraint.ConstrSys.EqConstrSys

module HM : Batteries.Hashtbl.S with type key = S.v

module VS : Batteries.Set.S with type elt = S.v

Signature

type data

type eq_wrapper = S.v -> ((S.v -> S.d -> unit) -> S.d) -> S.d

val create_empty_data : unit -> data

val copy_marshal : data -> data

val relift_marshal : data -> data

val register_start : data -> S.v -> S.d -> unit

val get_wrapper : 
  solve_widen:(S.v -> unit) ->
  init:(S.v -> unit) ->
  stable:unit HM.t ->
  data:data ->
  sides:VS.t HM.t ->
  add_sides:(S.v -> S.v -> unit) ->
  rho:S.d HM.t ->
  destabilize:(S.v -> unit) ->
  side:(?x:S.v -> S.v -> S.d -> unit) ->
  assert_can_receive_side:(S.v -> unit) ->
  eq_wrapper