Carsten Sinz
2012-Aug-31 17:51 UTC
[LLVMdev] Announcement: Version 2012.2 of LLBMC available
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>
Seemingly Similar Threads
- [LLVMdev] Announcement: LLBMC, the Low-Level Bounded Model Checker
- [LLVMdev] Announcement: LLBMC, the Low-Level Bounded Model Checker
- [LLVMdev] Announcement: LLBMC, the Low-Level Bounded Model Checker
- [LLVMdev] Announcement: Version 2013.1 of LLBMC available
- [LLVMdev] Modifying the support CommandLine Library to support option categories and iteration over registered options