Linux Driver Verification » BLAST

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).