1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
import java.lang.RuntimeException;
import org.cprover.CProver;
public class Sync
{
public int field;
public static void main(String[] args)
{
final Sync o = new Sync();
o.field = 0;
// test regular synchronized method (monitorexit on return)
o.f();
// test synchronized method with throw (monitorexit on catch)
try
{
o.g();
}
catch (RuntimeException e)
{
o.field++;
}
// Make sure both functions were executed and the second threw
// The object should remain unlocked
if ((o.field !=3) || (CProver.getMonitorCount(o) !=0))
assert(false);
}
public synchronized void f()
{
// Check that we acquired the lock
if (CProver.getMonitorCount(this) !=1)
assert(false);
field++;
}
public synchronized void g()
{
field++;
// Check that we acquired the lock
if (CProver.getMonitorCount(this) !=1)
assert(false);
throw new RuntimeException();
}
}
|
