KeYProject / key

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

IssueDialog with PositionedStrings with undefined Locations #3518

Open BookWood7th opened 4 days ago

BookWood7th commented 4 days ago
## Description The Location class may be instantiated without an associated file. This causes fileUri to be null. Due to this Location::compareTo causes a NullPointerException, when used by a Location without an associated file ## Reproducible always ### Steps to reproduce > Describe the steps needed to reproduce the issue. 1. Create a Location without an associated fileUri (Location.UNDEFINED / any constructor values with fileUri set to null) 2. Create a second Location object 3. call compareTo on the first Location comparing it to the second Expected to sort by their Position objects. Actually throws NullPointerException. ### Additional information --- * Commit:

8e28439

BookWood7th commented 4 days ago

The issue actually does not concern Location but instead IssueDialog where sorting is done without checking for these NullPointerExceptions. May also be an edge case of Java documentation for Array.sort, which can't take Comparators that don't accept null values

mattulbrich commented 2 days ago

Well, compareTo should not fail for valid argument objects, so I'd say it is a bug in the comparison.

Probably easy to fix by making the comparison null-aware, isn't it?

BookWood7th commented 10 hours ago

The issue is reasonably easy to fix and I believe I found a somewhat elegant solution to this. The proposed solution adds explicit nullsLast comparators that check for null values of fileUri and position fields in Location before using the respective natural order of these fields in Location#compareTo(Location)