-
Notifications
You must be signed in to change notification settings - Fork 348
/
TwoResourcesECM.java
41 lines (36 loc) · 1.42 KB
/
TwoResourcesECM.java
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
// A test case for https://github.com/typetools/checker-framework/issues/4838.
//
// This test that shows that no unsoundess occurs when a single close() method is responsible
// for closing two resources.
import java.io.IOException;
import java.net.Socket;
import org.checkerframework.checker.calledmethods.qual.*;
import org.checkerframework.checker.mustcall.qual.*;
@InheritableMustCall("dispose")
class TwoResourcesECM {
@Owning Socket s1, s2;
// The contracts.postcondition error below is thrown because s1 is not final,
// and therefore might theoretically be side-effected by the call to s2.close()
// even on the non-exceptional path. See ReplicaInputStreams.java for a variant
// of this test where such an error is not issued. Because this method can leak
// along both regular and exceptional exits, both errors are issued.
//
// The contracts.exceptional.postcondition error is thrown because destructors
// have to close their resources even on exception. If s1.close() throws an
// exception, then s2.close() will not be called.
@EnsuresCalledMethods(
value = {"this.s1", "this.s2"},
methods = {"close"})
// :: error: (contracts.postcondition)
// :: error: (contracts.exceptional.postcondition)
public void dispose() throws IOException {
s1.close();
s2.close();
}
static void test1(TwoResourcesECM obj) {
try {
obj.dispose();
} catch (IOException ioe) {
}
}
}