search

KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
42 stars 24 forks source link

Nullness Type System activated for `key.ncore` #3468

Closed wadoon closed 2 months ago

wadoon commented 2 months ago

Nullness type checker activated in key.ncore.

wadoon commented 2 months ago

@flo2702 It compiles now. On key.ncore, the checker framework is misconfigured.

If I enable the ENABLE_NULLNESS, I get an error in ImmutableMap<K,V>. 

/home/weigl/work/key/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java:13: error: [type.argument.type.incompatible] incompatible type argument for type parameter S of ImmutableMapEntry.
        extends Iterable<ImmutableMapEntry<S, T>>, java.io.Serializable {
                                           ^
  found   : S[ extends @UnknownKeyFor Object super @KeyForBottom Void]
  required: [extends @UnknownKeyFor Object super @UnknownKeyFor NullType]
flo2702 commented 2 months ago

Do we write @Nullable private T field or private @Nullable T field? (Same question applies to method return types)

I prefer the second option. Unless you have strong reasons for the first option, I will change this before merging.

wadoon commented 2 months ago

Do we write @Nullable private T field or private @Nullable T field? (Same question applies to method return types)

I have no preferences. And for me this is also no quality issue.

Maybe a good reformatter can reformat this.