[clang] [StaticAnalyzer] early return if sym is concrete on assuming (PR #115579)
Ding Fei via cfe-commits
cfe-commits at lists.llvm.org
Mon Nov 11 08:34:55 PST 2024
================
@@ -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
More information about the cfe-commits
mailing list