Install the CStar toolchain. If cstarc is not found when the extension
activates, it offers to download and install the toolchain for you; you can
also run the CStar IDE: Download CStar Toolchain command at any time.
Make sure the cstarc binary is on your PATH, or set Cstar: Path to the directory that
contains it. The server resolves its include / lib runtime directories
relative to the binary, so keep the standard layout.
Fix your configuration in Settings
Cstar: Path
This extension depends on the clangd
extension, which VS Code installs automatically. Set Clangd: Path
(clangd.path) to cst_clangd, the clangd binary distributed within the
CStar toolchain, so C language features match the CStar dialect. If you
also have Microsoft's C/C++ extension installed, disable it — it conflicts
with clangd, and the extension will warn you on activation.
Start the HOL server by running the CStar IDE: Start HOL Light Server
command. It serves on 127.0.0.1:7000 by default.
Show Symbolic State
Show the symbolic state and in-scope variables at the current line:
Open your CStar file.
Make sure the HOL server is running, and you may need to restart it from time to time.
Move your cursor to the line of interest, then run the CStar IDE: Show Symbolic State
command (keybinding Ctrl+Alt+Right, or Alt+Right on Linux).
The panel shows the enclosing function, its symbolic state, and the in-scope
ghost variables grouped by scope; each section is collapsible, and an
unchanged section keeps its fold/unfold status across updates.
When the server also returns verification conditions, they
appear as an additional collapsible section in the same panel, alongside the
symbolic state and scopes.
The code from the top of the file through the queried line is backlit in the
editor to show what has been symbolically executed so far. The backlight rolls
back to the line before your edit when you change the highlighted region, and
clears when the file is closed.
Stop Symbolic State Daemon
To speed up repeated queries, the server keeps a warm incremental-verification
daemon per file. If it gets into a bad state, run the CStar IDE: Stop Symbolic State Daemon command (keybinding Ctrl+Alt+Left, or Alt+Left on Linux)
to tear down the daemon for the backlit file (or the active file)
and clear the backlight; the next Show Symbolic State respawns a fresh one.
