Conversation
Previously, DefExc used the widening operator as implemented by Lattice.StdCousot -- which is not a valid widening operator (as of now), because if it just returns the second argument.
|
We maybe should consider to simply remove |
|
Searching for Line 69 in 0a88b34 So, as it's used currently, it shouldn't be unsound (except for slr3 maybe).
We should probably just remove |
There are not really any good default implementations for narrowing and (in particular) for widening that can be defined by a module.
…/ narrow If something includes another domain and then redefines join (meet), widen (narrow) needs to be redefined as well
|
Ok, now that @michael-schwarz fixed it, should we just merge this? |
|
Apparently this behavior was intended and the solvers are written in a way such that they always did a |
This was erroneously changed to `narrow = meet` in #97
Previously,
DefExcused the widening operator as implemented byLattice.StdCousot-- which is not a valid widening operator (as of now), because it just returns the second argument:analyzer/src/domains/lattice.ml
Lines 35 to 39 in 0a88b34
So now we define the
widensimply by thejoinforDefExc.More generally speaking, there are 16 includes of
StdCousotin the code base (not counting those inarrayDomain_deprecatedandintDomain_unused). At some of these places, thewidenmight not be overridden and the resulting behavior might be unsound.