================
@@ -23,7 +23,14 @@ RangedConstraintManager::~RangedConstraintManager() {}
ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
SymbolRef Sym,
bool Assumption) {
- Sym = simplify(State, Sym);
+ SVal SimplifiedVal = simplifyToSVal(State, Sym);
----------------
NagyDonat wrote:
I have a vague feeling that we're adding more and more _ad hoc_ simplification
calls when we realize that they are needed and something is buggy without them.
(E.g. I added them to `SimpleSValBuilder::get{Min,Max}Value` when I introduced
those functions a few months ago.)
Although I support these changes individually and I don't think that they are
problematic, perhaps it would be even better to review and refactor the
handling of symbolic values to ensure that they are simplified once when it's
necessary.
Obviously this would be a big work, but it could be part of a more general
symbol handling improvement -- there are many inconsistencies in our logic
(e.g. we assume that signed overflow is possible and normal; we don't always
recognize commutativity and associativity of addition and similar operations;
there are bugs related to casting; we cannot deduce that `a == b` and `c == d`
implies `a+c == b+d`; AFAIK we cannot deduce that `a < b` and `b < c` implies
`a < c`) and eventually we should clear out many of these out in a single major
improvement.
https://github.com/llvm/llvm-project/pull/115579
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
