| // A test for some issues related to the getFD() method in RandomAccessFile. |
| |
| import java.io.*; |
| import org.checkerframework.checker.mustcall.qual.*; |
| |
| class FileDescriptors { |
| void test(@Owning RandomAccessFile r) throws Exception { |
| @MustCall("close") FileDescriptor fd = r.getFD(); |
| // :: error: assignment |
| @MustCall({}) FileDescriptor fd2 = r.getFD(); |
| } |
| |
| void test2(@Owning RandomAccessFile r) throws Exception { |
| @MustCall("close") FileInputStream f = new FileInputStream(r.getFD()); |
| // :: error: assignment |
| @MustCall({}) FileInputStream f2 = new FileInputStream(r.getFD()); |
| } |
| } |