Closed Baltoli closed 7 years ago
Make sure that no call to release dominates any other call to release - if this is the case, then the lock would be released multiple times.
Instead of dominance, I think we want the more conservative analysis of reachability - if we can statically reach another release call, then the analysis should report a failure.
Make sure that no call to release dominates any other call to release - if this is the case, then the lock would be released multiple times.