You may download sources and binaries on the Files page of the BLAST project. See also the original project page.
Release notes¶
This version only inroduces a few new options to support SV-COMP'14
competition rules:
- "
-alias empty" to disable alias analysis ("-alias ''" is sometimes hard to specify)
- "
-errorpathfile file" to print resulting (final) error trace to file
- "
-propertyfile file" to read .prp property from the file specified
You may download sources and binaries on the Files page of the BLAST project. See also the original project page.
Release notes¶
This version fixes a couple of bugs exposed at the Competition on Software Verification at TACAS'12. We advise you to use 2.7.1 instead of 2.7.
Analysis¶
- Fix bug that all undefined local variables, such as int __VERIFIER_nondet_int() { int val; return val; }, were treated as equal in all calls of a function.
Infrastructure improvements¶
- Binary builds are now compatible with RHEL 5.
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).
You may download sources and binaries on the Files page of the project. See also the original project page.
Release notes¶
Analysis speedup¶
- Speedup ranges from 8 times on small-sized programs to 30 times on medium-sized programs
- Logarithmic algorithm for useful-blocks (significantly speedup of trace analysis)
- Improved integration with SMT solvers
- efficient string concatenation
- caching of converted formulae
- optimization of CVC3 options for BLAST use cases
- Formulae normalization has been moved to solvers since solvers do it faster (option
-skipnorm)
- Alias analysis speedup
- must-aliases are handled separately and faster than may-aliases (option
-nomusts)
- removed unnecessary debug prints from alias iteration (even a check for debug flag impacts performance significantly in hot places)
- BLAST-specific tuning of OCaml virtual machine options (script
"ocamltune")
Important bug fixes¶
- Fixed unsound analysis when lattices are used (options
-stop-sep and -merge) (Time of analysis has been increased by a factor of 1.5, but the inherent imprecision in lattices no longer makes BLAST miss bugs). See bug #330
- bool-to-int casting in function calls fixed. See bug #334
Frontend¶
- C frontend (CIL) uplift, fixes and workarounds (see
-ignoredupfn and -nosserr options)
- Some errors have been made warnings
New features¶
- constrain stack depth to be analyzed; see options
-fdepth, -important-attrs, and -inline-attrs
- treat constant pointers as must aliases (see option
-const)
Infrastructure improvements¶
- Regression test suite improved
- Got rid of non-free software (Simplify solver was replaced by CVC3, ditched unused Vampyre, FOCI, and CLPprover)