Package cbmc
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 |