cbmc

Bounded model checker for C programs with static analysis

brewmacoslinux

Try with needOr install directly

About

C Bounded Model Checker

cbmcgoto-ccgoto-instrument

Check a C program for buffer overflows and assertion violations$ cbmc program.c

Verify a specific function with loop unwinding limit$ cbmc program.c --function main --unwind 5

Generate goto-binary for further analysis$ goto-cc -o program.gb program.c