| import org.checkerframework.checker.lock.qual.*; |
| |
| public class Methods { |
| |
| final Object lock = new Object(); |
| |
| @Holding("lock") |
| void lockedByLock() {} |
| |
| @Holding("this") |
| void lockedByThis() {} |
| |
| // unguarded calls |
| void unguardedCalls() { |
| // :: error: (contracts.precondition) |
| lockedByLock(); // error |
| // :: error: (contracts.precondition) |
| lockedByThis(); // error |
| } |
| |
| @Holding("lock") |
| void usingHolding1() { |
| lockedByLock(); |
| // :: error: (contracts.precondition) |
| lockedByThis(); // error |
| } |
| |
| @Holding("this") |
| void usingHolding2() { |
| // :: error: (contracts.precondition) |
| lockedByLock(); // error |
| lockedByThis(); |
| } |
| |
| void usingSynchronization1() { |
| synchronized (lock) { |
| lockedByLock(); |
| // :: error: (contracts.precondition) |
| lockedByThis(); // error |
| } |
| } |
| |
| void usingSynchronization2() { |
| synchronized (this) { |
| // :: error: (contracts.precondition) |
| lockedByLock(); // error |
| lockedByThis(); |
| } |
| } |
| |
| synchronized void usingMethodModifier() { |
| // :: error: (contracts.precondition) |
| lockedByLock(); // error |
| lockedByThis(); |
| } |
| } |