Skip to content

The CBMC proof debugger is a Visual Studio Code extension contributing a trace debugger for findings by CBMC.

License

Notifications You must be signed in to change notification settings

jaisnan/cbmc-proof-debugger

 
 

Repository files navigation

CBMC Proof Debugger

The CBMC Proof Debugger is a Visual Studio Code debugger for CBMC error traces.

CBMC is a model checker for C. CBMC will explore all possible paths through your code on all possible inputs, and will check that all assertions in your code are true. CBMC can also check for the possibility of security issues (like buffer overflow) and for instances of undefined behavior (like signed integer overflow). If CBMC finds a code issue, it generates an error trace demonstrating how that issue could occur. If CBMC terminates without finding any issues, the result is assurance that your code behaves as expected. CBMC is a bounded model checker, however, so getting CBMC to terminate may require restricting inputs to some bounded size, and CBMC's assurance is restricted to these bounded inputs.

CBMC Viewer is a tool that scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues CBMC finds using any web browser. Viewer also produces a summary of its findings in the form of a collection of json blobs.

The CBMC Proof Debugger loads the json summaries produced by CBMC Viewer, and lets a developer explore the error traces produced by CBMC using the Visual Studio Code's debugger.

The user guide includes a simple demonstration of the debugger.

Security

See CONTRIBUTING for more information.

License

This library is licensed under the MIT-0 License. See the LICENSE file.

About

The CBMC proof debugger is a Visual Studio Code extension contributing a trace debugger for findings by CBMC.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • TypeScript 99.5%
  • Makefile 0.5%