| package pkg2; |
| |
| import org.checkerframework.framework.testchecker.util.EnsuresOdd; |
| import org.checkerframework.framework.testchecker.util.Odd; |
| import org.checkerframework.framework.testchecker.util.RequiresOdd; |
| import pkg1.Class1; |
| |
| public class Class2 { |
| @RequiresOdd("Class1.field") |
| // :: error: (flowexpr.parse.error) |
| public void requiresOddParseError() { |
| // :: error: (assignment) |
| @Odd Object odd = Class1.field; |
| } |
| |
| @RequiresOdd("pkg1.Class1.field") |
| public void requiresOdd() { |
| @Odd Object odd = Class1.field; |
| } |
| |
| @EnsuresOdd("Class1.field") |
| // :: error: (flowexpr.parse.error) |
| public void ensuresOddParseError() { |
| // :: warning: (cast.unsafe.constructor.invocation) |
| Class1.field = new @Odd Object(); |
| } |
| |
| @EnsuresOdd("pkg1.Class1.field") |
| public void ensuresOdd() { |
| // :: warning: (cast.unsafe.constructor.invocation) |
| Class1.field = new @Odd Object(); |
| } |
| |
| void illegalUse() { |
| // :: error: (contracts.precondition) |
| requiresOdd(); |
| } |
| |
| void legalUse() { |
| // :: warning: (cast.unsafe.constructor.invocation) |
| Class1.field = new @Odd Object(); |
| requiresOdd(); |
| } |
| } |