njit-jerse / specimin

SPECIfication MINimizer. A different kind of slicer for Java.
MIT License
3 stars 7 forks source link

Specimin's modularity model does not match NullAway's with respect to fields #332

Open kelloggm opened 4 months ago

kelloggm commented 4 months ago

NullAway's rules for fields require that all non-null fields be initialized before a constructor completes. The modularity model that NullAway is using here differs from the one that Specimin currently implements (based on the Checker Framework's typechecking rules) in the following ways:

I think this means we need to introduce a separate modularity model for NullAway that reflects these differences.

This is the reason that Specimin currently does not preserve na-323, even with the change in #331.

kelloggm commented 4 months ago

Partially fixed (first bullet point) by #345.