Skip to content

Commit 698c06b

Browse files
authored
Add doc section on debugging Kani in VS code (rust-lang#1294)
1 parent 81c5b67 commit 698c06b

File tree

1 file changed

+19
-0
lines changed

1 file changed

+19
-0
lines changed

docs/src/rustc-hacks.md

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,25 @@ You may also need to install the `rustc-dev` package using rustup
3333
rustup toolchain install nightly --component rustc-dev
3434
```
3535

36+
#### Debugging in VS code
37+
38+
To debug Kani in VS code, first install the [CodeLLDB extension](https://marketplace.visualstudio.com/items?itemName=vadimcn.vscode-lldb).
39+
Then add the following lines at the start of the `main` function (see [the CodeLLDB manual](https://github.com/vadimcn/vscode-lldb/blob/master/MANUAL.md#attaching-debugger-to-the-current-process-rust) for details):
40+
41+
```rust
42+
{
43+
let url = format!(
44+
"vscode://vadimcn.vscode-lldb/launch/config?{{'request':'attach','sourceLanguages':['rust'],'waitFor':true,'pid':{}}}",
45+
std::process::id()
46+
);
47+
std::process::Command::new("code").arg("--open-url").arg(url).output().unwrap();
48+
}
49+
```
50+
51+
Note that pretty printing for the Rust nightly toolchain (which Kani uses) is not very good as of June 2022.
52+
For example, a vector may be displayed as `vec![{...}, {...}]` on nightly Rust, when it would be displayed as `vec![Some(0), None]` on stable Rust.
53+
Hopefully, this will be fixed soon.
54+
3655
### CLion / IntelliJ
3756
This is not a great solution, but it works for now (see <https://github.com/intellij-rust/intellij-rust/issues/1618>
3857
for more details).

0 commit comments

Comments
 (0)