SMACK v2.3.0

Release notes:

• updated to LLVM 7.1.0

SMACK v2.2.0

Release notes:

• switched to LLVM 6.0.1

SMACK v2.1.0

Release notes:

• switched to LLVM 5.0.2
• removing temporary files in case of sigterm

SMACK v2.0.0

Release notes:

• using clang-format to enforce LLVM code style
• improved handling of LLVM intrinsics
• switched to LLVM 4.0.1
• added format characters to __SMACK_code
• moved prelude generation into llvm2bpl
• bug fixes

SMACK v1.9.3

Release notes:

• last minute SVCOMP-related patch

SMACK v1.9.2

Release notes:

• SVCOMP improvements
• bug fixes

SMACK v1.9.1

Release notes:

• experimental support for multi- and cross-language verification (Fortran, Objective-C, D, etc.)
• prototype verification of Rust programs
• extended support for handling of floating-points, including modeling of C math library
• improved memory safety checking
• support for modeling of vector instructions
• modeling of C string library
• bug fixes

SMACK v1.9.0

Release notes:

• switched to LLVM 3.9
• added regression testing for checking Boogie files and verifier outputs
• added metadata annotations to distinguish instructions that are only related to verification
• added a pass that records data useful for security timing analysis
• better support for dealing with LLVM IR structs
• implemented portable library models
• bug fixes

SMACK v1.8.1

Release notes:

• Hotfix release with bug fixes for APLAS paper

SMACK v1.8.0

Release notes:

• switched to LLVM 3.8
• added support for Travis CI
• added functionality for replaying of error traces
• bug fixes