viperproject / viperserver

HTTP server that manages verification requests to different tools from the Viper tool stack.
Other
10 stars 17 forks source link

Minor: change exception reports to include runnable commands/quoted paths #106

Open alexanderjsummers opened 1 year ago

alexanderjsummers commented 1 year ago

When the backend crashes unexpectedly, the output from Viper Server includes messages such as:

The command carbon --z3Exe c:\Users\Alex Summers\AppData\Roaming\Code\User\globalStorage\viper-admin.viper\Nightly\ViperTools\z3\bin\z3.exe --boogieExe c:\Users\Alex Summers\AppData\Roaming\Code\User\globalStorage\viper-admin.viper\Nightly\ViperTools\boogie\Binaries\Boogie.exe resulted in an exception.

It would be great if this could be improved by (a) including quotes etc. around paths (as they are presumably written in the underlying command) and (b) including the (properly quoted) path to the file being verified. This way, the output could be taken and rerun locally when debugging (and potential confusion with the paths looking broken could be avoided, of course!).