New version (2012.2) of LLBMC available

Skip to first unread message


Aug 31, 2012, 1:12:42 PM8/31/12
We are very pleased to announce that a new version of LLBMC is available
for download at!

LLBMC is a high-precision static analyzer implementing a technique 
called "Bounded Model Checking". LLBMC is based on LLVM and 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

Reply all
Reply to author
0 new messages