| import org.checkerframework.checker.calledmethods.qual.*; |
| |
| public class Xor { |
| |
| class Foo { |
| void a() {} |
| |
| void b() {} |
| |
| void c() {} |
| // SPEL doesn't support XOR directly (it represents exponentiation as ^ instead), |
| // so use a standard gate encoding |
| void aXorB(@CalledMethodsPredicate("(a || b) && !(a && b)") Foo this) {} |
| } |
| |
| void test1(Foo f) { |
| // :: error: method.invocation |
| f.aXorB(); |
| } |
| |
| void test2(Foo f) { |
| f.c(); |
| // :: error: method.invocation |
| f.aXorB(); |
| } |
| |
| void test3(Foo f) { |
| f.a(); |
| f.aXorB(); |
| } |
| |
| void test4(Foo f) { |
| f.b(); |
| f.aXorB(); |
| } |
| |
| void test5(Foo f) { |
| f.a(); |
| f.b(); |
| // :: error: method.invocation |
| f.aXorB(); |
| } |
| |
| void callA(Foo f) { |
| f.a(); |
| } |
| |
| void test6(Foo f) { |
| callA(f); |
| f.b(); |
| // DEMONSTRATION OF UNSOUNDNESS |
| f.aXorB(); |
| } |
| |
| void test7(@CalledMethods("a") Foo f) { |
| f.aXorB(); |
| } |
| |
| void test8(Foo f) { |
| callA(f); |
| // THIS IS AN UNAVOIDABLE FALSE POSITIVE |
| // :: error: method.invocation |
| f.aXorB(); |
| } |
| } |