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 over 7 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