package goblint
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=20d5b7332a9f6072ab9ba86c4a53b898eaf681286c56a8805c41850bbf3ddf41
sha512=7c7685cfcd9aa866bc40e813df2bfcb3c79b3d40e615d8d6d0939c5798b9d70dd7f2ba87a741f5ba0ce891e9d254627207fb28057f1f2f6611e4e0d128fd6a71
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