| // Checks that annotations from the Value Checker (which is a subchecker of the WPI test checker) |
| // are actually present in the generated files, even when there is also an annotation from the main |
| // checker. |
| |
| import org.checkerframework.checker.testchecker.wholeprograminference.qual.Sibling1; |
| import org.checkerframework.common.value.qual.IntVal; |
| |
| public class ValueCheck { |
| |
| // return value should be @Sibling1 @IntVal(5) int |
| int getSibling1withValue5() { |
| return ((@Sibling1 int) 5); |
| } |
| |
| void requireSibling1(@Sibling1 int x) {} |
| |
| void requireIntVal5(@IntVal(5) int x) {} |
| |
| void test() { |
| int x = getSibling1withValue5(); |
| // :: warning: argument |
| requireSibling1(x); |
| // :: warning: argument |
| requireIntVal5(x); |
| } |
| } |