================
@@ -23,7 +23,14 @@ RangedConstraintManager::~RangedConstraintManager() {}
ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
SymbolRef Sym,
bool Assumption) {
- Sym = simplify(State, Sym);
+ SVal SimplifiedVal = simplifyToSVal(State, Sym);
+ if (SimplifiedVal.isConstant()) {
+ bool Feasible = SimplifiedVal.isZeroConstant() ? !Assumption : Assumption;
----------------
danix800 wrote:
Maybe `Assumption ? !SimplifiedVal.isZeroConstant() :
SimplifiedVal.isZeroConstant()` is more clear, which reads more naturally like:
```c
if (SimplifiedVal) {
// ...
}
```
being translated into
```c
if (Assumption) // you want SimplifiedVal to be true?
Feasible = !SimplifiedVal.isZeroConstant(); // ok, then it SHOULD NOT be zero
else
Feasible = SimplifiedVal.isZeroConstant(); // no, then it SHOULD be zero
```
Honestly I made a truth table to aid in understanding the equivalence of all
these forms:
|Assume|isZero|isZero != Assume|Assume ? !isZero : isZero | isZero ? !Assume :
Assume |
|---|---|---|---|---|
|T|T|F|F|F|
|T|F|T|T|T|
|F|T|T|T|T|
|F|F|F|F|F|
And YES! they are equivalent!
But I'll choose the shortest one as you suggested! Thanks!
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
