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!).
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.exeresulted 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!).