| import org.checkerframework.framework.test.*; |
| import org.checkerframework.framework.testchecker.util.*; |
| |
| public class MetaPostcondition { |
| |
| String f1, f2, f3; |
| MetaPostcondition p; |
| |
| /** *** normal postcondition ***** */ |
| @EnsuresOdd("f1") |
| void oddF1() { |
| f1 = null; |
| } |
| |
| @EnsuresOdd("p.f1") |
| void oddF1_1() { |
| p.f1 = null; |
| } |
| |
| @EnsuresOdd("#1.f1") |
| void oddF1_2(final MetaPostcondition param) { |
| param.f1 = null; |
| } |
| |
| @EnsuresOdd("f1") |
| // :: error: (contracts.postcondition) |
| void oddF1_error() {} |
| |
| @EnsuresOdd("---") |
| // :: error: (flowexpr.parse.error) |
| void error() {} |
| |
| @EnsuresOdd("#1.#2") |
| // :: error: (flowexpr.parse.error) |
| void error2(final String p1, final String p2) {} |
| |
| @EnsuresOdd("f1") |
| void exception() { |
| throw new RuntimeException(); |
| } |
| |
| @EnsuresOdd("#1") |
| void param1(final @Odd String f) {} |
| |
| @EnsuresOdd({"#1", "#2"}) |
| // :: error: (flowexpr.parameter.not.final) |
| void param2(@Odd String f, @Odd String g) { |
| f = g; |
| } |
| |
| @EnsuresOdd("#1") |
| // :: error: (flowexpr.parse.index.too.big) |
| void param3() {} |
| |
| // basic postcondition test |
| void t1(@Odd String p1, String p2) { |
| // :: error: (assignment) |
| @Odd String l1 = f1; |
| oddF1(); |
| @Odd String l2 = f1; |
| |
| // :: error: (flowexpr.parse.error.postcondition) |
| error(); |
| } |
| |
| // test parameter syntax |
| void t2(@Odd String p1, String p2) { |
| // :: error: (flowexpr.parse.index.too.big) |
| param3(); |
| } |
| |
| // postcondition with more complex expression |
| void tn1(boolean b) { |
| // :: error: (assignment) |
| @Odd String l1 = p.f1; |
| oddF1_1(); |
| @Odd String l2 = p.f1; |
| } |
| |
| // postcondition with more complex expression |
| void tn2(boolean b) { |
| MetaPostcondition param = null; |
| // :: error: (assignment) |
| @Odd String l1 = param.f1; |
| oddF1_2(param); |
| @Odd String l2 = param.f1; |
| } |
| |
| // basic postcondition test |
| void tnm1(@Odd String p1, @Value String p2) { |
| // :: error: (assignment) |
| @Odd String l1 = f1; |
| // :: error: (assignment) |
| @Value String l2 = f2; |
| |
| // :: error: (flowexpr.parse.error.postcondition) |
| error2(p1, p2); |
| } |
| |
| /** conditional postcondition */ |
| @EnsuresOddIf(result = true, expression = "f1") |
| boolean condOddF1(boolean b) { |
| if (b) { |
| f1 = null; |
| return true; |
| } |
| return false; |
| } |
| |
| @EnsuresOddIf(result = false, expression = "f1") |
| boolean condOddF1False(boolean b) { |
| if (b) { |
| return true; |
| } |
| f1 = null; |
| return false; |
| } |
| |
| @EnsuresOddIf(result = false, expression = "f1") |
| boolean condOddF1Invalid(boolean b) { |
| if (b) { |
| f1 = null; |
| return true; |
| } |
| // :: error: (contracts.conditional.postcondition) |
| return false; |
| } |
| |
| @EnsuresOddIf(result = false, expression = "f1") |
| // :: error: (contracts.conditional.postcondition.returntype) |
| void wrongReturnType() {} |
| |
| @EnsuresOddIf(result = false, expression = "f1") |
| // :: error: (contracts.conditional.postcondition.returntype) |
| String wrongReturnType2() { |
| f1 = null; |
| return ""; |
| } |
| |
| // basic conditional postcondition test |
| void t3(@Odd String p1, String p2) { |
| condOddF1(true); |
| // :: error: (assignment) |
| @Odd String l1 = f1; |
| if (condOddF1(false)) { |
| @Odd String l2 = f1; |
| } |
| // :: error: (assignment) |
| @Odd String l3 = f1; |
| } |
| |
| // basic conditional postcondition test (inverted) |
| void t4(@Odd String p1, String p2) { |
| condOddF1False(true); |
| // :: error: (assignment) |
| @Odd String l1 = f1; |
| if (!condOddF1False(false)) { |
| @Odd String l2 = f1; |
| } |
| // :: error: (assignment) |
| @Odd String l3 = f1; |
| } |
| |
| // basic conditional postcondition test 2 |
| void t5(boolean b) { |
| condOddF1(true); |
| if (b) { |
| // :: error: (assignment) |
| @Odd String l2 = f1; |
| } |
| } |
| } |