search

goblint / GobPie

Goblint IDE integration via MagpieBridge
MIT License
5 stars 3 forks source link

Mode to show only one warning per message group #45

Closed karoliineh closed 1 year ago

karoliineh commented 1 year ago

Here is the non-explosive related messages mode that @vesalvojdani requested #44.

There is now a "secret" option explodeGroupWarnings in GobPie, which is true by default, meaning, that if the option is not set in the configuration file or is set to true, the group warnings are exploded as they were previously.

When this option is set to false, however, GobPie will only generate one warning per message group, with all its pieces as related warnings. If the group message has a location provided by Goblint, it is shown in that location. Otherwise, a random location of one of the pieces is taken. If none of the pieces has a location, it will be handled the same as all other warnings without locations.

I hope it also works for @sim642 because GobPie is not making too many decisions here. If Goblint eventually will sort and prioritize accesses, the relevant location can be passed with the group location, or the method that randomly selects the location right now can be rewritten to use the location provided by Goblint by some other means.

Pros: the "Problems" view looks just like Goblint's command line output. Cons: only the location where the group warning sits is highlighted, but one can jump around through the location links in the related warnings.

sim642 commented 1 year ago

If the group message has a location provided by Goblint, it is shown in that location.

Groups don't have a location field themselves though, only group text. For races that text happens to contain the variable's location in already stringified form.

Or does the repositioning branch have some change which this assumes?

karoliineh commented 1 year ago

Groups don't have a location field themselves though, only group text. For races that text happens to contain the variable's location in already stringified form.

Or does the repositioning branch have some change which this assumes?

Hah, that is actually a good question. I just now realized, that I have mashed up the variant types into one class in GobPie since the very beginning so I didn't even think of the Group not having a location currently. https://github.com/goblint/GobPie/blob/33e82f51a817b2d56d9e7ceba70e0bc3c61416a0/src/main/java/api/messages/GoblintMessagesResult.java#L66-L71

Should I look into some way to actually separate them?

The repositioning branch does not yet have a location for groups, but I am planning on adding it. The GobPie implementation still works with the location being always missing, but I will soon enough make use of it assuming that a group can indeed have a location.