search

goblint / GobPie

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

Possibility to use goblint conf file #7

Closed karoliineh closed 2 years ago

karoliineh commented 2 years ago

Needed for issues #2 and #5.

Running the plugin now assumes goblint is added to the PATH.

When there is a goblint conf file with the name "goblint.json" present in the project root directory, the plugin uses it to run the command. If the conf file is not present, the default command is still: goblint --enable dbg.debug --set result json-messages -o <pathToJsonResult> <fileToAnalyze>

karoliineh commented 2 years ago

Is there a better way than just throwing an exception to let the extension user know if they don't have goblint in their PATH? Same with the goblint.json not being in a correct format etc. Right now, it is very easy to break the extension, and as a user, it is pretty tricky to find out why the extension does not work when there is something wrong.

https://github.com/goblint/GobPie/blob/941896f5e0584134762c2ed37eda2d36cc2c291c/src/main/java/GoblintAnalysis.java#L119-L124

sim642 commented 2 years ago

When there is a goblint conf file with the name "goblint.json" present in the project root directory, the plugin uses it to run the command. If the conf file is not present, the default command is still: goblint --enable dbg.debug --set result json-messages -o <pathToJsonResult> <fileToAnalyze>

If goblint.json isn't present, then the plugin shouldn't do anything with C files. It's quite annoying to have it automatically run on every C file you ever open with VSCode. For example, even developing Goblint itself and looking at its regression tests, the plugin tries to run and show warnings, but the default configuration is incorrect for those. Or to look at a repository like sv-benchmarks which has tens of thousands of C programs.

sim642 commented 2 years ago

Is there a better way than just throwing an exception to let the extension user know if they don't have goblint in their PATH? Same with the goblint.json not being in a correct format etc. Right now, it is very easy to break the extension, and as a user, it is pretty tricky to find out why the extension does not work when there is something wrong.

Does Magpie not provide any way to show custom alerts to the user? Like the ones that say something like "Goblint started/finished analyzing file".

karoliineh commented 2 years ago

Is there a better way than just throwing an exception to let the extension user know if they don't have goblint in their PATH? Same with the goblint.json not being in a correct format etc. Right now, it is very easy to break the extension, and as a user, it is pretty tricky to find out why the extension does not work when there is something wrong.

Does Magpie not provide any way to show custom alerts to the user? Like the ones that say something like "Goblint started/finished analyzing file".

That was a good idea. Added the notifications that notify the user when there is an error with running the goblint command with the last commit.

linghuiluo commented 2 years ago

Hi, it is great to see you are using MagpieBridge! Definitely let me know (create an issue) if you want new features!