| import org.checkerframework.framework.testchecker.testaccumulation.qual.*; |
| |
| public class Xor { |
| |
| class Foo { |
| void a() {} |
| |
| void b() {} |
| |
| void c() {} |
| // use a standard gate encoding for xor |
| void aXorB(@TestAccumulationPredicate("(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(@TestAccumulation("a") Foo f) { |
| f.aXorB(); |
| } |
| |
| void test8(Foo f) { |
| callA(f); |
| // THIS IS AN UNAVOIDABLE FALSE POSITIVE |
| // :: error: method.invocation |
| f.aXorB(); |
| } |
| } |