cbmc: cbmc (C Bounded Model Checker)
cbmc:
cbmc:   CBMC is a Bounded Model Checker for C and C++ programs. It supports
cbmc: C89, C99, most of C11/C17 and most compiler extensions provided by
cbmc: gcc and clang.
cbmc:   CBMC verifies memory safety (which includes array bounds checks and
cbmc: checks for the safe use of pointers), checks for exceptions, checks
cbmc: for various variants of undefined behavior, and user-specified
cbmc: assertions.
cbmc:   Compiled with native SAT solver Cadical:
cbmc: https://www.cprover.org/cbmc     https://github.com/arminbiere/cadical