Announcement: Version 2012.2 of LLBMC available

We are very pleased to announce that a new version of LLBMC is available
for download at

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