diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueIgnoreRangeOverflowTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueIgnoreRangeOverflowTest.java index afd06a041383..a50a74f83569 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueIgnoreRangeOverflowTest.java +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueIgnoreRangeOverflowTest.java @@ -2,6 +2,7 @@ import org.checkerframework.common.value.ValueChecker; import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.checkerframework.framework.test.TestUtilities; import org.junit.runners.Parameterized.Parameters; import java.io.File; @@ -20,6 +21,7 @@ public ValueIgnoreRangeOverflowTest(List testFiles) { "value", // Ignore the test suite's usage of qualifiers in illegal locations. "-AignoreTargetLocations", + TestUtilities.adapt("-Astubs=tests/value/unchecked-bytecode.astub"), "-A" + ValueChecker.REPORT_EVAL_WARNS, "-A" + ValueChecker.IGNORE_RANGE_OVERFLOW); } diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueTest.java index 01579f71a5e0..bd06c7daa6c3 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueTest.java +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueTest.java @@ -28,7 +28,9 @@ public ValueTest(List testFiles) { // Ignore the test suite's usage of qualifiers in illegal locations. "-AignoreTargetLocations", TestUtilities.adapt( - "-Astubs=tests/value/minints-stub.astub:tests/value/lowercase.astub"), + "-Astubs=tests/value/minints-stub.astub" + + ":tests/value/lowercase.astub" + + ":tests/value/unchecked-bytecode.astub"), "-A" + ValueChecker.REPORT_EVAL_WARNS); } diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java index d33bdf51dd8e..f9d836539d24 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/ValueUncheckedDefaultsTest.java @@ -20,7 +20,8 @@ public ValueUncheckedDefaultsTest(List testFiles) { "value", // Ignore the test suite's usage of qualifiers in illegal locations. "-AignoreTargetLocations", - "-AuseConservativeDefaultsForUncheckedCode=btyecode", + "-Astubs=tests/value/unchecked-bytecode.astub", + "-AuseConservativeDefaultsForUncheckedCode=bytecode", "-A" + ValueChecker.REPORT_EVAL_WARNS); } diff --git a/framework/tests/value/StringSplit.java b/framework/tests/value/StringSplit.java index aba7942c2786..1c063cc18103 100644 --- a/framework/tests/value/StringSplit.java +++ b/framework/tests/value/StringSplit.java @@ -6,6 +6,7 @@ public class StringSplit { void needsALR1(String @ArrayLenRange(from = 1) [] arg) {} void g(String compiler) { + // :: error: (argument.type.incompatible) needsALR1(compiler.trim().split(" +")); } diff --git a/framework/tests/value/unchecked-bytecode.astub b/framework/tests/value/unchecked-bytecode.astub new file mode 100644 index 000000000000..b3f51796243d --- /dev/null +++ b/framework/tests/value/unchecked-bytecode.astub @@ -0,0 +1,235 @@ +package java.lang; + +import org.checkerframework.common.value.qual.ArrayLen; +import org.checkerframework.common.value.qual.ArrayLenRange; +import org.checkerframework.common.value.qual.StringVal; +import org.checkerframework.common.value.qual.UnknownVal; + +class Math { + static int min(@UnknownVal int a, @UnknownVal int b); + + static long min(@UnknownVal long a, @UnknownVal long b); + + static float min(@UnknownVal float a, @UnknownVal float b); + + static double min(@UnknownVal double a, @UnknownVal double b); + + static int max(@UnknownVal int a, @UnknownVal int b); + + static long max(@UnknownVal long a, @UnknownVal long b); + + static float max(@UnknownVal float a, @UnknownVal float b); + + static double max(@UnknownVal double a, @UnknownVal double b); +} + +class String { + static String format(@UnknownVal String format, @UnknownVal Object... args); + + String(@UnknownVal byte[] bytes); + + String(@UnknownVal char[] value); + + String(@UnknownVal char[] value, @UnknownVal int offset, @UnknownVal int count); + + boolean equalsIgnoreCase(@UnknownVal String anotherString); + + int indexOf(@UnknownVal int ch); + + int indexOf(@UnknownVal int ch, @UnknownVal int fromIndex); + + int indexOf(@UnknownVal String str, @UnknownVal int fromIndex); + + String replace(@UnknownVal char oldChar, @UnknownVal char newChar); + + String substring(@UnknownVal int beginIndex); + + String substring(@UnknownVal int beginIndex, @UnknownVal int endIndex); + + String @ArrayLenRange(from = 0) [] split(@UnknownVal String regex); + + boolean startsWith(@UnknownVal String prefix); + + boolean endsWith(@UnknownVal String suffix); + + static @StringVal({"true", "false"}) String valueOf(@UnknownVal boolean b); + + static @ArrayLen(1) String valueOf(@UnknownVal char c); + + static @ArrayLenRange(from = 1, to = 11) String valueOf(@UnknownVal int i); + + static @ArrayLenRange(from = 1, to = 20) String valueOf(@UnknownVal long l); +} + +class StringBuilder { + StringBuilder append(@UnknownVal char c); + + StringBuilder append(@UnknownVal String str); +} + +package java.io; + +import org.checkerframework.common.value.qual.UnknownVal; + +class PrintStream { + void print(@UnknownVal String s); + + void print(@UnknownVal char c); + + void println(@UnknownVal Object x); + + void println(@UnknownVal String x); + + void println(@UnknownVal int x); +} + +class IOException { + IOException(@UnknownVal String message); +} + +package java.lang; + +import org.checkerframework.common.value.qual.UnknownVal; + +class ClassLoader { + Class loadClass(@UnknownVal String name) throws ClassNotFoundException; +} + +class Class { + Class asSubclass(@UnknownVal Class clazz); +} + +class Object { + boolean equals(@UnknownVal Object obj); +} + +class IllegalArgumentException { + IllegalArgumentException(@UnknownVal String s); +} + +class UnsupportedOperationException { + UnsupportedOperationException(@UnknownVal String message); +} + +class RuntimeException { + RuntimeException(@UnknownVal String message, @UnknownVal Throwable cause); +} + +class AssertionError { + AssertionError(@UnknownVal Object detailMessage); +} + +class Error { + Error(@UnknownVal String message); +} + +package org.checkerframework.framework.testchecker.lib; + +import org.checkerframework.common.value.qual.StaticallyExecutable; +import org.checkerframework.common.value.qual.UnknownVal; + +class VarargsMethods { + @StaticallyExecutable + static int test0(@UnknownVal Object... objects); + + @StaticallyExecutable + static int test1(@UnknownVal String s, @UnknownVal Object... objects); + + @StaticallyExecutable + static int test2(@UnknownVal String s, @UnknownVal String s2, @UnknownVal Object... objects); +} + +package java.util; + +import org.checkerframework.common.value.qual.UnknownVal; + +class Arrays { + static List asList(@UnknownVal T... a); +} + +class ArrayList { + ArrayList(@UnknownVal Collection c); +} + +class Collections { + static > T min(@UnknownVal Collection coll); + + static T min( + @UnknownVal Collection coll, @UnknownVal Comparator comp); + + static Collection checkedCollection( + @UnknownVal Collection c, @UnknownVal Class type); + + static > void sort(@UnknownVal List list); +} + +class HashSet { + HashSet(@UnknownVal Collection c); + + boolean contains(@UnknownVal Object o); +} + +interface Set { + boolean retainAll(@UnknownVal Collection c); +} + +package java.nio.file; + +import org.checkerframework.common.value.qual.UnknownVal; + +class Paths { + static Path get(@UnknownVal String first, @UnknownVal String... more); +} + +class Files { + static java.io.BufferedWriter newBufferedWriter( + @UnknownVal Path path, @UnknownVal java.nio.charset.Charset cs, @UnknownVal OpenOption... options); + + static boolean isRegularFile(@UnknownVal Path path, @UnknownVal LinkOption... options); +} + +package java.lang.invoke; + +import org.checkerframework.common.value.qual.UnknownVal; + +class MethodHandle { + Object invoke(@UnknownVal Object... args) throws Throwable; +} + +package java.util.stream; + +import org.checkerframework.common.value.qual.UnknownVal; + +interface Stream { + static Stream of(@UnknownVal T... values); + + R collect(@UnknownVal Collector collector); + + Stream skip(@UnknownVal long n); + + Stream sorted(@UnknownVal java.util.Comparator comparator); + + java.util.Optional max(@UnknownVal java.util.Comparator comparator); +} + +interface IntStream { + static IntStream range(@UnknownVal int startInclusive, @UnknownVal int endExclusive); +} + +class Collectors { + static Collector joining(@UnknownVal CharSequence delimiter); + + static Collector> toMap( + @UnknownVal java.util.function.Function keyMapper, + @UnknownVal java.util.function.Function valueMapper); + + static > Collector toMap( + @UnknownVal java.util.function.Function keyMapper, + @UnknownVal java.util.function.Function valueMapper, + @UnknownVal java.util.function.BinaryOperator mergeFunction, + @UnknownVal java.util.function.Supplier mapSupplier); + + static Collector collectingAndThen( + @UnknownVal Collector downstream, + @UnknownVal java.util.function.Function finisher); +}