package goblint

  1. Overview
  2. Docs

Module Td3UpdateRule.InactiveSource

Parameters

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

Signature

Sourcetype data
Sourcetype eq_wrapper = S.v -> ((S.v -> S.d -> unit) -> S.d) -> S.d
Sourceval create_empty_data : unit -> data
Sourceval copy_marshal : data -> data
Sourceval relift_marshal : data -> data
Sourceval register_start : data -> S.v -> S.d -> unit
Sourceval 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