We are very pleased to announce that a new version of LLBMC is available
for download at http://llbmc.org.
LLBMC is a high-precision static analyzer based on LLVM implementing a
technique called "Bounded Model Checking". LLBMC can detect errors such as:
- Illegal memory accesses (e.g., buffer overflows)
- Integer overflows
- Division by zero
- Invalid bit shifts
- Double frees
The new version, 2012.2, offers several new features and improvements:
- Extended support for C library functions. LLBMC now has built-in support for:
memcpy, memset, memmove, strlen, strcpy, strncpy, strcat, strncat, strchr,
memchr, strcmp, strncmp, memcmp, toupper, tolower, malloc, calloc, free,
exit, abort
- New options: --max-builtins-iterations, --max-memcpy-iterations, --memcpy=<method>
- New, additional output format: SMTLIB (versions 1 and 2)
- Support for many GCC/LLVM built-in functions (e.g., __builtin_parity())
- Improved counterexample traces
- LLBMC is now based on LLVM 3.1
- New version of STP (revision 1666)
- Support for backend solver "MiniSat and propagators" in STP
- Option --friendly-protoypes renamed to --ignore-missing-function-bodies
- General stability and performance improvements