[LLVMdev] Announcement: Version 2013.1 of LLBMC available

Carsten Sinz carsten.sinz at kit.edu
Thu Jun 20 09:35:17 PDT 2013


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, 2013.1, offers several new features and improvements:

- LLBMC now performs lazy, on-demand loop unrolling, function inlining, and
  encoding

- LLBMC can now take several bitcode files as input and it is no longer necessary
  to use llvm-link in order to combine them into a single bitcode file

- Improved status information output

- LLBMC is now based on LLVM 3.3

- New version of STP (revision 1673)

- General stability and performance improvements
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20130620/559d000f/attachment.html>
-------------- 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/20130620/559d000f/attachment.bin>


More information about the llvm-dev mailing list