Skink Program Verification Tool
Visual Studio Code Language Server support for the Skink program verification tool.
Anthony M. Sloane
Programming Languages and Verification Research Group, Department of Computing, Macquarie University
If you have a Skink development directory building correctly then you should be able to use the extension. See Setup below for configuration.
In detail, you will need:
Adjust Skink settings. At least the following will need to be setup the first time:
These other settings can be adjusted as desired:
The Skink language server starts automatically when you open a C file. When a C file is opened or saved, Skink will be run to verify that file. Diagnostics will indicate the results of the verification.
By default, Skink will verify the
The Skink sidebar provides access to a lot of information about the verification process. Under the "Products" heading there will be one entry for each file that has been verified and is still open. Browse under that entry to find detailed descriptions of the verification results, witness values, LLVM code and control flow graphs, and log files.
Some of the products shown in the Skink sidebar are linked back to the original C file. E.g., clicking on an instruction in the "program LLVM" product will focus the C code from which that instruction came. The "Skink: Focus Product Editors" can be used to focus in the other direction: select a location in the C file, run the command, and you should see selections on relevant product text.