SideWPointSelect (goblint.Goblint_solver.SideWPointSelect)

module type S =
  functor (S : ConstrSys.EqConstrSys) ->
  functor (HM : Batteries.Hashtbl.S with type key = S.v) ->
  functor (VS : Batteries.Set.S with type elt = S.v) ->
  sig ... end

module Always : S

Any side-effect after the first one will be widened which will unnecessarily lose precision.

module Never : S

Never widen side-effects.

module SidesLocal : S

Widening check happens by checking sides. Only widen if value increases and there has already been a side-effect from the same source

module SidesPP : S

If there was already a `side x y d` from the same program point and now again, make y a widening point. Different from `Sides` in that it will not distinguish between side-effects from different contexts, only the program point matters.

module Sides : S

If there already was a `side x y d` that changed rhoy and now again, we make y a wpoint. x caused more than one update to y. >=3 partial context calls will be precise since sides come from different x. TODO this has 8 instead of 5 phases of `solver` for side_cycle.c

module UnstableSelf : S

Side to y destabilized itself via some infl-cycle. Records influences from unknowns to globals

module UnstableCalled : S

Widen if any called var (not just y) is no longer stable. Expensive!

module Cycle : S

Destabilized a called or start var. Problem: two partial context calls will be precise, but third call will widen the state. If this side destabilized some of the initial unknowns vs, there may be a side-cycle between vs and we should make y a wpoint

val choose_impl : unit -> (module S)