model-checking/kani-vscode-extension

Kani extension appears to crash when stack size is too small

jaisnan opened this issue · 2 comments

The extension appears to get stuck if the stack size is too small. This can appear as a test case looping infinitely.

The current workaround for the issue is to do the following.

The user can set the environment variable COMPlus_DefaultStackSize to a sufficiently large value before starting VSCode. For example:

# Increase the stack size
export COMPlus_DefaultStackSize=100000
# Launch VSCode
code

OR

stop the verification using the stop button on the testing panel.

In case the extension takes a long time to verify, and the stack size is not a viable solution, users might want a timeout feature that lets someone know how long or where verification is taking. This is a feature that's to be implemented in Kani itself but at the extension level, it's much easier to pop up a notification window asking users if they want to close the current process.