package goblint
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=af01aac256229f33a90a9fcbfed04b01e3097f154d4d124f006476d6387c6a66
sha512=2a93bfe16881adbc2d8dcbfe38c1e19cd24ca105d8e1eda13d02440f3002874ffe2957dfd937510765233a054a40568b0052db92e31d382a5bd215d1ec12565c
doc/goblint.solver/Goblint_solver/SideWPointSelect/index.html
Module Goblint_solver.SideWPointSelectSource
Strategies for widening leaf unknowns
module type S =
functor (S : Goblint_constraint.ConstrSys.EqConstrSys) ->
functor (HM : Batteries.Hashtbl.S with type key = S.v) ->
functor (VS : Batteries.Set.S with type elt = S.v) ->
sig ... endAny side-effect after the first one will be widened which will unnecessarily lose precision.
Widening check happens by checking sides. Only widen if value increases and there has already been a side-effect from the same source
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.
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
Side to y destabilized itself via some infl-cycle. Records influences from unknowns to globals
Widen if any called var (not just y) is no longer stable. Expensive!
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