Project

General

Profile

BLAST 2.7 has been released

BLAST 2.7 has been released as a result of improvements made within Linux Driver Verification program and for the purpose to take part in Competition on Software Verification at TACAS'12.
Added by Alexey Khoroshilov over 7 years ago

You may download sources and binaries on the Files page of the project. See also the original project page.

Release notes

Analysis speedup

  • Fast and sound algorithm for alias analysis for pointers to structures without dereference depth limit enforced. Does not terminate on some programs with arbitrary-depth lists.
  • Add some normalization for better caching of postcondition requests.
  • Improved performance of lattice states merge.

New features

  • Re-animated function pointer support (-fp), which, however, doesn't distpatch correctly two or more functions aliased by the pointer.
  • Updated 64- and 32-bit versions of CSIsat allow you to analyze programs with as large numbers as your architecture supports.

Infrastructure improvements

  • Separated supported and unsupported options. Most recently added options has been made default.
  • Regression test suite may work in "competition" mode.

Bug fixes

  • Formulae caching in O(logN) useful blocks algorithm fixed (less FOCIinterface.SAT exceptions).

Comments