smack

Release notes:

• improved support for precise reasoning about floating-point numbers
• fine-tuned SV-COMP 2017 heuristics
• bug fixes

Release notes:

• improved support for precise reasoning about floating-point numbers
• implemented support for memory safety checking of global memory
• fine-tuned SV-COMP 2017 heuristics
• bug fixes

Release notes:

• improved checking of memory safety
• implemented support for precise reasoning about floating-point numbers
• switched to LLVM 3.7
• bug fixes

Release notes:

• implemented checking of memory safety
• switched to LLVM 3.6
• removed GNU make based build
• created documentation folder
• implemented a script for running SMACK from a virtual machine
• bug fixes

Release notes:

• improved handling of function pointers and functions with variable number of arguments
• experimental support for pthreads
• refactored SMACK scripts
• refactored memory models
• improved support for code contracts (preconditions, postconditions, loop invariants)
• competing in SVCOMP 2016
• bug fixes

Release notes:

• support for bit vector operations and reasoning
• precise handling of byte-level memory accesses
• portable build using Vagrant
• refactored regression system
• switched to using SVCOMP-like __VERIFIER_XXX helper functions
• support for running SMACK on projects with multiple files
• bug fixes

Release notes:

• updated SMACK to LLVM 3.5
• experimental feature: code contracts (preconditions, postconditions, loop invariants)
• support for Duality verification engine
• experimental support for C++
• support for computing reachability of program statements (thanks to Montgomery Carter)
• annotating error traces with concrete values of program variables
• wrote a script for packaging SMACK using CDE
• bug fixes

Release notes:

• cleaned up memory models (removed twodim memory model); also, memory models can now be changed without changing and recompiling SMACK since they are mostly specified as separate SMACK headers
• SMACK parameters can now be specified per file in comments using SMACK-OPTIONS keyword
• created a build script for Ubuntu 14.04
• implemented smackreach script that computes code reachability info using SMACK (thanks to Montgomery Carter)
• updated rise4fun examples (thanks to Arvind Haran)
• implemented a new memory model that allows memory reuse when malloc is invoked
• implemented support for memset and memcpy
• bug fixes

Release notes:

• upgraded SMACK to LLVM 3.4
• implemented support for writing Boogie code directly in C programs, which is convenient for modeling (see https://github.com/smackers/smack/wiki#wiki-writing-boogie-code-directly-in-c-programs)
• updated SMACK to be a standalone LLVM tool instead of a pass (thanks to Pantazis Deligiannis)
• support building SMACK with cmake (thanks to Pantazis Deligiannis)
• improved automatic build scripts to deal with mono/Boogie/Corral discrepancies
• bug fixes

Release notes:

• Minor fix to make SMACK work on the MacOS Mavericks

Release notes:

• splitting memory based on the results of alias analysis (DSA)
• handling static global initialization
• supporting Corral as another back-end verifier
• upgraded to LLVM 3.3
• bug fixes