1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
// This class should not issues any errors, since these annotations are identical to the ones
// on java.io.PrintWriter in the Index JDK.
import java.io.File;
import java.io.FileNotFoundException;
import java.io.PrintWriter;
import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.IndexOrHigh;
public class MethodOverrides3 extends PrintWriter {
public MethodOverrides3(File file) throws FileNotFoundException {
super(file);
}
@Override
public void write(char[] buf, @IndexFor("#1") int off, @IndexOrHigh("#1") int len) {}
}
|
