search

goblint / GobPie

Goblint IDE integration via MagpieBridge
MIT License
7 stars 4 forks source link

Handle results with empty locations #22

Closed karoliineh closed 2 years ago

karoliineh commented 2 years ago

The fix for #21.

Depending on what Magpie allows, there are a few choices:

  1. Completely ignore locationless messages.
  2. If possible, output the message such that it's in the warnings list, but nowhere in the analyzed source code.
  3. If the previous is not possible, then alternative might be to attach some location to it to have it show up somewhere.

The solution I did is something between options 2 and 3. I first tried with an empty position, but at least sourcefileURL must be not null in the position, otherwise, MagpieBridge will run into exception. When adding just the project source directory URL for sourcefileURL, the message will be completely ignored (only the messages with line numbers present will be shown). Then I added line and column numbers with values 1, which gives a solution that shows the warning in the warning list, but nowhere in the analyzed source file (2), however it still has to have some location attached to it (3).

image

The only problem is that the warning in the warnings list is not connected to any file, because as the loc field is completely empty, I cannot get the filename from there (from loc.file). Therefore one has to guess for which file the warning is connected. The other problem is, that when clicking on the warning, you get an error pop-up Unable to open 'DemoProject': File is a directory. from VSCode, because the position has the project directory as the sourcefileURL.

If the loc.file field would be always available, this issue with the result not being connected to a file would be solved, but it would bring another problem: some line and column numbers must still be given. Therefore I should put 1 for their values as in the current solution so that the warnings without locations would be always shown on the first line of the file. This might cause problems when the file is empty, but I guess a file in VSCode always has at least one line in it so it shouldn't actually be a problem? Edit: also I guess there are no warnings in an empty file anyways? So maybe it is possible to make the loc.file to never be empty?

karoliineh commented 2 years ago

Yes, the fallback new File("") currently gives the project root.