Announcement: Version 2013.1 of LLBMC available

Project Infrastructure LLVM Dev List Archives
1

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