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 about 10 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