| import org.checkerframework.checker.initialization.qual.*; |
| import org.checkerframework.checker.nullness.qual.*; |
| |
| // This test does not correctly work in the FBC system, |
| // see https://github.com/typetools/checker-framework/issues/223 |
| class RawField { |
| |
| public @UnknownInitialization RawField a; |
| |
| public RawField() { |
| // :: error: (assignment) |
| a = null; |
| this.a = this; |
| a = this; |
| } |
| |
| // :: error: (initialization.fields.uninitialized) |
| public RawField(boolean foo) {} |
| |
| void t1() { |
| // :: error: (method.invocation) |
| a.t1(); |
| } |
| |
| void t2(@UnknownInitialization RawField a) { |
| this.a = a; |
| } |
| } |
| |
| class Options { |
| |
| @UnknownInitialization Object arg; |
| |
| public Options(@UnknownInitialization Object arg) { |
| this.arg = arg; |
| } |
| |
| public void parse_or_usage() { |
| // use arg only under the assumption that it is @UnknownInitialization |
| } |
| } |
| |
| class MultiVersionControl { |
| |
| @SuppressWarnings("nullness") // see https://github.com/typetools/checker-framework/issues/223 |
| public void parseArgs(@UnknownInitialization MultiVersionControl this) { |
| Options options = new Options(this); |
| options.parse_or_usage(); |
| } |
| } |
| |
| // TODO: This checks that forbidden field assignments do not occur. (The |
| // FBC type system permits arbitrary assignments in a constructor, but it |
| // also makes assumptions that our implementation does not currently check.) |
| // class HasStaticUnknownInitializationField { |
| // static @UnknownInitialization Object f; |
| // } |
| // |
| // class UseUnknownInitializationField { |
| // |
| // Object f; |
| // |
| // public UseUnknownInitializationField() { |
| // // :: (initialization.field.write.in.constructor) |
| // f = HasStaticUnknownInitializationField.f; |
| // } |
| // |
| // } |