| import org.checkerframework.dataflow.qual.Pure; |
| import org.checkerframework.framework.qual.RequiresQualifier; |
| import org.checkerframework.framework.test.*; |
| import org.checkerframework.framework.testchecker.util.*; |
| |
| // various tests for the precondition mechanism |
| public class FieldShadowing { |
| |
| String f; |
| |
| class Sub extends FieldShadowing { |
| String f; |
| |
| @Pure |
| @RequiresQualifier(expression = "f", qualifier = Odd.class) |
| int reqSub() { |
| @Odd String l2 = f; |
| // :: error: (assignment) |
| @Odd String l1 = super.f; |
| int i; |
| i = 1; |
| return 1; |
| } |
| |
| @Pure |
| @RequiresQualifier(expression = "super.f", qualifier = Odd.class) |
| int reqSuper() { |
| // :: error: (assignment) |
| @Odd String l2 = f; |
| @Odd String l1 = super.f; |
| return 1; |
| } |
| |
| void t1(@Odd String p1) { |
| f = p1; |
| // :: error: (contracts.precondition) |
| reqSuper(); |
| reqSub(); |
| } |
| |
| void t2(@Odd String p1) { |
| super.f = p1; |
| // :: error: (contracts.precondition) |
| reqSub(); |
| reqSuper(); |
| } |
| } |
| } |