[LLVMdev] Announcement: Version 2012.2 of LLBMC available

[Carsten Sinz]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4880 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20120831/17cf10d6/attachment.bin>