Bounded Model Checker for ANSI-C and C++ programs
CBMC generates traces that demonstrate how an assertion can be violated, or
proves that the assertion cannot be violated within a given number of loop
iterations.
Version: 5.95.1
General Commands | |
| cbmc | Bounded Model Checker for C/C++ and Java programs |
| crangler | C source transformation |
| goto-analyzer | Data-flow analysis for C programs and goto binaries |
| goto-cc | C/C++ to goto compiler |
| goto-diff | Syntactic diff of goto binaries |
| goto-gcc | alias for goto-cc |
| goto-harness | Generate environments for symbolic analysis |
| goto-instrument | Perform analysis or instrumentation of goto binaries |
| goto-ld | alias for goto-cc |
| goto-synthesizer | Synthesize and apply loop contracts of goto binaries. |
| memory-analyzer | Snapshot program state for symbolic analysis |
| symtab2gb | Compile JSON symbol tables to a GOTO binary |