Project

General

Profile

BLAST 2.6 has been released

The first final version 2.6 of ISPRAS edition of BLAST has been released. The tool is a development of BLAST 2.5 released in 2008.
Added by Pavel Shved 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

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

Comments