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.
- 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.
- 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.
- Separated supported and unsupported options. Most recently added options has been made default.
- Regression test suite may work in "competition" mode.
- Formulae caching in O(logN) useful blocks algorithm fixed (less FOCIinterface.SAT exceptions).