================
@@ -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.
----------------
steakhal wrote:
You are saying that in some cases the constraints of only one of the bifurcated
state gets simplified.
This is really odd to me. How I remember (and always try to reason about) the
constraint system of every State is simplified. Consequently, we are never
delayed of realizing when we get overly constrained given a system. We always
know what constraint caused a chain of perfect constraints that lead to the
deduction of an impossible situation (that we were already overly constrained)
So let me ask this directly, have you seen a case where the constraint system
wasn't simplified after adding a constraint to it?
https://github.com/llvm/llvm-project/pull/210912
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
