smack

Release notes:

• updated to LLVM 12.0.1
• updated Boogie and Z3
• switched to main branch instead of master
• support for adding assertions after loops (to catch not unrolling enough)
• improved error trace generation
• cleanup of Rust panic
• bug fixes

Release notes:

• support for externalizing of entry points
• updated Boogie and Corral verifiers
• improved error trace generation
• removed virtual SMACK installation option
• targeted function checking
• bug fixes

Release notes:

• updated to LLVM 11.1.0
• modeling of Rust's memory functions
• GitHub actions are now creating Docker images
• supporting Rust cargo compilation flow
• refactored warning messages
• bug fixes

Release notes:

• switched to using GitHub Actions for CI
• bug fixes
• improved SVCOMP heuristics

Release notes:

• minor fix to modeling of bit-wise operations using integers

Release notes:

• added support for Ubuntu 20.04
• updated Boogie, Corral, and Z3
• cleaned up SVCOMP heuristics
• implemented support for Rust cargo
• model bit-wise operations as integer operations when possible
• cleaned up SVCOMP witness generation

Release notes:

• updated to LLVM 10.0.1
• updated CVC4 and SeaDsa

Release notes:

• updated to LLVM 9.0.1
• implemented sound modeling of integer wrapping
• refactored integer modeling flags
• check Python formatting during CI
• reformatted Python scripts
• updated Z3, Boogie, Corral

Release notes:

• replaced LLVM's old DSA with SeaDSA
• made allocation to be atomic
• upgraded to Python 3
• modularized Corral and Boogie dependencies
• integrated Rust regressions into the test folder
• refactored regressions into separate folders based on input language

Release notes:

• updated to LLVM 8.0.1
• updated Vagrant and Docker to Ubuntu 18.04

Release notes:

• updated to LLVM 7.1.0

Release notes:

• switched to LLVM 6.0.1

Release notes:

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

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

Release notes:

• last minute SVCOMP-related patch

Release notes:

• SVCOMP improvements
• bug fixes

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

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

Release notes:

• Hotfix release with bug fixes for APLAS paper

Release notes:

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