================
@@ -493,8 +493,11 @@ void PthreadLockChecker::AcquireLockAux(const CallEvent
&Call,
default:
llvm_unreachable("Unknown tryLock locking semantics");
}
- assert(lockFail && lockSucc);
- C.addTransition(lockFail);
+ // The state where the lock failed can be infeasible if the constraint
+ // solver only now discovers a contradiction in the accumulated
+ // constraints; only take that transition when it is feasible.
----------------
necto wrote:
I believe in the C case, the simplification is attempted but fails because
`simplify` is expected to return a symbol:
```C++
SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
SVal SimplifiedVal = simplifyToSVal(State, Sym);
if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol())
return SimplifiedSym;
return Sym;
}
```
And in this case, it simplifies to a ConcreteInt, so it falls back to
unsimplified `Sym` and does not attempt further simplification, because the
full constraint simplification is triggered only when we add a concrete
equality like `x == 1`, and in this case the added constraint does not fit this
shape.
However, I don't know the details of constraint reasoning in CSA deep enough to
judge if there should have been some other simplification taking place.
https://github.com/llvm/llvm-project/pull/210912
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
