| import org.checkerframework.dataflow.qual.Pure; |
| import org.checkerframework.framework.qual.EnsuresQualifier; |
| import org.checkerframework.framework.qual.EnsuresQualifierIf; |
| import org.checkerframework.framework.test.*; |
| import org.checkerframework.framework.testchecker.util.*; |
| |
| public class Postcondition { |
| |
| String f1, f2, f3; |
| Postcondition p; |
| |
| @Pure |
| String p1() { |
| return null; |
| } |
| |
| /** *** normal postcondition ***** */ |
| @EnsuresQualifier(expression = "f1", qualifier = Odd.class) |
| void oddF1() { |
| f1 = null; |
| } |
| |
| @EnsuresQualifier(expression = "p.f1", qualifier = Odd.class) |
| void oddF1_1() { |
| p.f1 = null; |
| } |
| |
| @EnsuresQualifier(expression = "#1.f1", qualifier = Odd.class) |
| void oddF1_2(final Postcondition param) { |
| param.f1 = null; |
| } |
| |
| @EnsuresQualifier(expression = "p.p1()", qualifier = Odd.class) |
| void oddF1_3() { |
| if (p.p1() == null) { |
| return; |
| } |
| throw new RuntimeException(); |
| } |
| |
| @EnsuresQualifier(expression = "f1", qualifier = Value.class) |
| // :: error: (contracts.postcondition) |
| void valueF1() {} |
| |
| @EnsuresQualifier(expression = "---", qualifier = Value.class) |
| // :: error: (flowexpr.parse.error) |
| void error() {} |
| |
| @EnsuresQualifier(expression = "#1.#2", qualifier = Value.class) |
| // :: error: (flowexpr.parse.error) |
| void error2(final String p1, final String p2) {} |
| |
| @EnsuresQualifier(expression = "f1", qualifier = Value.class) |
| void exception() { |
| throw new RuntimeException(); |
| } |
| |
| @EnsuresQualifier(expression = "#1", qualifier = Value.class) |
| void param1(final @Value String f) {} |
| |
| @EnsuresQualifier( |
| expression = {"#1", "#2"}, |
| qualifier = Value.class) |
| // :: error: (flowexpr.parameter.not.final) |
| void param2(@Value String f, @Value String g) { |
| f = g; |
| } |
| |
| @EnsuresQualifier(expression = "#1", qualifier = Value.class) |
| // :: error: (flowexpr.parse.index.too.big) |
| void param3() {} |
| |
| // basic postcondition test |
| void t1(@Odd String p1, String p2) { |
| valueF1(); |
| // :: 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) { |
| Postcondition param = null; |
| // :: error: (assignment) |
| @Odd String l1 = param.f1; |
| oddF1_2(param); |
| @Odd String l2 = param.f1; |
| } |
| |
| // postcondition with more complex expression |
| void tn3(boolean b) { |
| // :: error: (assignment) |
| @Odd String l1 = p.p1(); |
| oddF1_3(); |
| @Odd String l2 = p.p1(); |
| } |
| |
| /** *** many postcondition ***** */ |
| @EnsuresQualifier.List({ |
| @EnsuresQualifier(expression = "f1", qualifier = Odd.class), |
| @EnsuresQualifier(expression = "f2", qualifier = Value.class) |
| }) |
| void oddValueF1(@Value String p1) { |
| f1 = null; |
| f2 = p1; |
| } |
| |
| @EnsuresQualifier(expression = "f1", qualifier = Odd.class) |
| @EnsuresQualifier(expression = "f2", qualifier = Value.class) |
| void oddValueF1_repeated1(@Value String p1) { |
| f1 = null; |
| f2 = p1; |
| } |
| |
| @EnsuresQualifier.List({ |
| @EnsuresQualifier(expression = "f1", qualifier = Odd.class), |
| }) |
| @EnsuresQualifier(expression = "f2", qualifier = Value.class) |
| void oddValueF1_repeated2(@Value String p1) { |
| f1 = null; |
| f2 = p1; |
| } |
| |
| @EnsuresQualifier(expression = "f1", qualifier = Odd.class) |
| @EnsuresQualifier.List({@EnsuresQualifier(expression = "f2", qualifier = Value.class)}) |
| void oddValueF1_repeated3(@Value String p1) { |
| f1 = null; |
| f2 = p1; |
| } |
| |
| @EnsuresQualifier.List({ |
| @EnsuresQualifier(expression = "f1", qualifier = Odd.class), |
| @EnsuresQualifier(expression = "f2", qualifier = Value.class) |
| }) |
| // :: error: (contracts.postcondition) |
| void oddValueF1_invalid(@Value String p1) {} |
| |
| @EnsuresQualifier.List({ |
| @EnsuresQualifier(expression = "--", qualifier = Odd.class), |
| }) |
| // :: error: (flowexpr.parse.error) |
| void error2() {} |
| |
| // basic postcondition test |
| void tnm1(@Odd String p1, @Value String p2) { |
| // :: error: (assignment) |
| @Odd String l1 = f1; |
| // :: error: (assignment) |
| @Value String l2 = f2; |
| oddValueF1(p2); |
| @Odd String l3 = f1; |
| @Value String l4 = f2; |
| |
| // :: error: (flowexpr.parse.error.postcondition) |
| error2(); |
| } |
| |
| /** *** conditional postcondition ***** */ |
| @EnsuresQualifierIf(result = true, expression = "f1", qualifier = Odd.class) |
| boolean condOddF1(boolean b) { |
| if (b) { |
| f1 = null; |
| return true; |
| } |
| return false; |
| } |
| |
| @EnsuresQualifierIf(result = false, expression = "f1", qualifier = Odd.class) |
| boolean condOddF1False(boolean b) { |
| if (b) { |
| return true; |
| } |
| f1 = null; |
| return false; |
| } |
| |
| @EnsuresQualifierIf(result = false, expression = "f1", qualifier = Odd.class) |
| boolean condOddF1Invalid(boolean b) { |
| if (b) { |
| f1 = null; |
| return true; |
| } |
| // :: error: (contracts.conditional.postcondition) |
| return false; |
| } |
| |
| @EnsuresQualifierIf(result = false, expression = "f1", qualifier = Odd.class) |
| // :: error: (contracts.conditional.postcondition.returntype) |
| void wrongReturnType() {} |
| |
| @EnsuresQualifierIf(result = false, expression = "f1", qualifier = Odd.class) |
| // :: error: (contracts.conditional.postcondition.returntype) |
| String wrongReturnType2() { |
| f1 = null; |
| return ""; |
| } |
| |
| @EnsuresQualifierIf(result = true, expression = "#1", qualifier = Odd.class) |
| boolean isOdd(final String p1) { |
| return isOdd(p1, 0); |
| } |
| |
| @EnsuresQualifierIf(result = true, expression = "#1", qualifier = Odd.class) |
| boolean isOdd(final String p1, int p2) { |
| return p1 == null; |
| } |
| |
| @EnsuresQualifierIf(result = false, expression = "#1", qualifier = Odd.class) |
| boolean isNotOdd(final String p1) { |
| return !isOdd(p1); |
| } |
| |
| // 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; |
| } |
| } |
| |
| /** *** many conditional postcondition ***** */ |
| @EnsuresQualifierIf.List({ |
| @EnsuresQualifierIf(result = true, expression = "f1", qualifier = Odd.class), |
| @EnsuresQualifierIf(result = false, expression = "f1", qualifier = Value.class) |
| }) |
| boolean condsOddF1(boolean b, @Value String p1) { |
| if (b) { |
| f1 = null; |
| return true; |
| } |
| f1 = p1; |
| return false; |
| } |
| |
| @EnsuresQualifierIf.List({ |
| @EnsuresQualifierIf(result = true, expression = "f1", qualifier = Odd.class), |
| @EnsuresQualifierIf(result = false, expression = "f1", qualifier = Value.class) |
| }) |
| boolean condsOddF1_invalid(boolean b, @Value String p1) { |
| if (b) { |
| // :: error: (contracts.conditional.postcondition) |
| return true; |
| } |
| // :: error: (contracts.conditional.postcondition) |
| return false; |
| } |
| |
| @EnsuresQualifierIf.List({ |
| @EnsuresQualifierIf(result = false, expression = "f1", qualifier = Odd.class) |
| }) |
| // :: error: (contracts.conditional.postcondition.returntype) |
| String wrongReturnType3() { |
| return ""; |
| } |
| |
| void t6(@Odd String p1, @Value String p2) { |
| condsOddF1(true, p2); |
| // :: error: (assignment) |
| @Odd String l1 = f1; |
| // :: error: (assignment) |
| @Value String l2 = f1; |
| if (condsOddF1(false, p2)) { |
| @Odd String l3 = f1; |
| // :: error: (assignment) |
| @Value String l4 = f1; |
| } else { |
| @Value String l5 = f1; |
| // :: error: (assignment) |
| @Odd String l6 = f1; |
| } |
| } |
| } |