@@ -22,6 +22,11 @@ abstract class LockingOperation extends FunctionCall {
2222 */
2323 abstract predicate isUnlock ( ) ;
2424
25+ /**
26+ * Holds if this locking operation can leak the lock. For example, RAII-style locks cannot leak.
27+ */
28+ abstract predicate canLeak ( ) ;
29+
2530 /**
2631 * Holds if this locking operation is really a locking operation within a
2732 * designated locking operation. This library assumes the underlying locking
@@ -33,11 +38,27 @@ abstract class LockingOperation extends FunctionCall {
3338 }
3439}
3540
41+ /**
42+ * A locking operation that can leak the lock.
43+ *
44+ * RAII style locks cannot leak, but other kinds of locks can.
45+ */
46+ abstract class LeakableLockingOperation extends LockingOperation {
47+ override predicate canLeak ( ) { any ( ) }
48+ }
49+
50+ /**
51+ * A locking operation that cannot leak the lock, such as RAII-style locks.
52+ */
53+ abstract class NonLeakableLockingOperation extends LockingOperation {
54+ override predicate canLeak ( ) { none ( ) }
55+ }
56+
3657/**
3758 * Common base class providing an interface into function call
3859 * based mutex locks.
3960 */
40- abstract class MutexFunctionCall extends LockingOperation {
61+ abstract class MutexFunctionCall extends LeakableLockingOperation {
4162 abstract predicate isRecursive ( ) ;
4263
4364 abstract predicate isSpeculativeLock ( ) ;
@@ -180,7 +201,7 @@ class CMutexFunctionCall extends MutexFunctionCall {
180201/**
181202 * Models a RAII-Style lock.
182203 */
183- class RAIIStyleLock extends LockingOperation {
204+ class RAIIStyleLock extends NonLeakableLockingOperation {
184205 VariableAccess lock ;
185206
186207 RAIIStyleLock ( ) {
0 commit comments