| import org.checkerframework.checker.initialization.qual.Initialized; |
| import org.checkerframework.checker.initialization.qual.UnderInitialization; |
| import org.checkerframework.checker.initialization.qual.UnknownInitialization; |
| import org.checkerframework.checker.nullness.qual.NonNull; |
| import org.checkerframework.checker.nullness.qual.Nullable; |
| |
| public class Commitment { |
| |
| @NonNull String t; |
| |
| // :: error: (initialization.field.type) |
| @NonNull @UnderInitialization String a; |
| // :: error: (initialization.field.type) |
| @Initialized String b; |
| @UnknownInitialization @Nullable String c; |
| |
| // :: error: (initialization.constructor.return.type) |
| public @UnderInitialization Commitment(int i) { |
| a = ""; |
| t = ""; |
| b = ""; |
| } |
| |
| // :: error: (initialization.constructor.return.type) |
| public @Initialized Commitment(int i, int j) { |
| a = ""; |
| t = ""; |
| b = ""; |
| } |
| |
| // :: error: (initialization.constructor.return.type) |
| // :: error: (nullness.on.constructor) |
| public @Initialized @NonNull Commitment(boolean i) { |
| a = ""; |
| t = ""; |
| b = ""; |
| } |
| |
| // :: error: (nullness.on.constructor) |
| public @Nullable Commitment(char i) { |
| a = ""; |
| t = ""; |
| b = ""; |
| } |
| |
| // :: error: (initialization.fields.uninitialized) |
| public Commitment() { |
| // :: error: (dereference.of.nullable) |
| t.toLowerCase(); |
| |
| t = ""; |
| |
| @UnderInitialization @NonNull Commitment c = this; |
| |
| @UnknownInitialization @NonNull Commitment c1 = this; |
| |
| // :: error: (assignment) |
| @Initialized @NonNull Commitment c2 = this; |
| } |
| |
| // :: error: (initialization.fields.uninitialized) |
| public Commitment(@UnknownInitialization Commitment arg) { |
| t = ""; |
| |
| // :: error: (argument) |
| @UnderInitialization Commitment t = new Commitment(this, 1); |
| |
| // :: error: (assignment) |
| @Initialized Commitment t1 = new Commitment(this); |
| |
| @UnderInitialization Commitment t2 = new Commitment(this); |
| } |
| |
| // :: error: (initialization.fields.uninitialized) |
| public Commitment(Commitment arg, int i) {} |
| } |