Skip to content
Choose a tag to compare

KLEE 2.0

@ccadar ccadar released this
· 448 commits to master since this release
Choose a tag to compare

KLEE 2.0, 19 March 2019

Incorporating changes from 22 July 2017 to 19 March 2019
Maintainers during this time span: @andreamattavelli, @ccadar, @delcypher, @MartinNowack
Documentation at

Major features

LLVM support

  • Added support for LLVM 3.7 - 7.0 (@jirislaby)
  • Added support for LLVM 8.0 (@MartinNowack)
  • KLEE 2.0 will be the last release with support for LLVM 3.4 to 3.7
  • Removed support for LLVM <3.4 (@MartinNowack)

Options, scripts and intrinsics changed or removed

  • Renamed several options (@ccadar)
    • --environ to --env-file
    • --no-output to --write-no-tests
    • --red-zone-space to --redzone-size
    • --run-in to --run-in-dir
    • --seed-out to --seed-file
    • --seed-out-dir to --seed-dir
    • --stop-after-n-tests to --max-tests
    • --use-cache to --use-branch-cache
    • --use-construct-hash to --use-construct-hash-stp
    • --warn-all-externals to --warn-all-external-symbols
  • Replaced --no-externals and --allow-external-sym-calls with --external-calls (@ccadar)
  • Added --libcxx option to enable LibC++ support (see Major features above)
  • Added option --max-stack-frames to limit the number of stack frames used (@MartinNowack)
  • Added --klee-call-optimisation option, which can be set to false to disable some optimizations that interact incorrectly with the checks injected by KLEE. See #1059 for more details (@MartinNowack)
  • Added support for disabling --batch-instructions and --batch-time by setting them to zero (@ccadar)
  • Removed option --disable-opt (@ccadar)
  • Removed klee-gcc and klee-clang (@251, @MartinNowack)
  • Removed support for klee_make_symbolic with two arguments (@ccadar)
  • Allow NULL as name to klee_int, to create "unnamed" object (@251)
  • New time API used in options (@251)
  • Improved the output of ktest-tool and added an --extract option (@251)
  • Categorized options in --help, improved help messages, and hid LLVM options by default (@ccadar)

Other changes

  • Updated build system to detect whether STP, Z3, metaSMT are available (@delcypher)
  • Fixed test case counter: previously the number of test cases generated by KLEE was always incremented, even if a symbolic solution was not found (@andreamattavelli)
  • Added checks for div/mod by zero and overshifts in constant expressions (@ccadar)
  • Fixed a bug causing KLEE to generate files with no permissions bits set (@ccadar)
  • Added clean_doxygen target and a global clean_all target to the build system (@delcypher)
  • Fixed initialization of distance to uncovered instructions when KLEE relies on default searchers (@andreamattavelli)
  • Fixed assert in BFSSearcher that does not hold as part of interleaved searcher (@jbuening)
  • Fixed huge allocation size constant (@davidtr1037)
  • Added Codecov support (@andreamattavelli, @MartinNowack)
  • Store cex cache stats and report them in klee-stats (@helicopter88)
  • Fixed incorrectly incremented stats for dumped states (@251)
  • Fixed bug where KLEE would not output test cases when --exit-on-error is enabled (@buszk)
  • Added support for blockaddress and indirectbr instructions (@251)
  • Implemented klee_prefer_cex() and klee_abort() for replay mode (@Lysxia)
  • Fixed handling of errno when external functions are invoked (@MartinNowack)
  • Fixed utimes() behavior for symbolic files when the second argument is NULL (@yxliang01)
  • Improved handling of constant array in Z3 (@kren1)
  • Improved the handling of external calls with symbolic data (@kren1)
  • Abort execution if --only-output-states-covering-new is enabled but its dependency --output-istats is not (@ccadar)
  • Improved ConstantExpr performance (@kren1)
  • Improved linking and optimizations order (@MartinNowack)
  • Enabled TCMalloc by default (@kren1)
  • Disabled unit testing in default build (@andreamattavelli)
  • Added resolve time to klee-stats --print-all (@251)
  • Improved the startup sequence enabling the POSIX runtime (@MartinNowack)
  • Added ASan and UBSan flags to lit (@251)
  • Added support for handling multiple SIGSEGVs in external calls (@251)
  • Added checks for correct usage of the POSIX mode (@ccadar)
  • Added support for klee-replay on OSX (@251)
  • Added lowering pass for atomic instructions (@erzett, @futile)
  • Improved handling of metadata (@MartinNowack)
  • Improved efficiency of div/mod and shift checks by skipping unnecessary checks (@MartinNowack)
  • Added support for memalign (@corrodedHash)
  • Enable C++14 support (@MartinNowack)
  • Fixed issue with aliases that point to other aliases (@jbuening)
  • Added workaround for the LLVM bug PR39177 (@jbuening)
  • Updated dependency build system for KLEE (@MartinNowack)
  • Fixed the Docker deployment for KLEE (@MartinNowack)
  • Added support for compiling KLEE with MSan and UBSan's integer sanitizer (@MartinNowack)
  • Fixed representation of ReadExpr's into equivalent arrays (@MartinNowack)
  • Added support for debug information provided by newer LLVM versions (@MartinNowack)
  • Added many KLEE-related publications (@251)
  • Smaller refactorings, fixes and improvements, test cases, maintenance,
    comments, web version, website, etc. (@andronat, @251, @andreamattavelli, @ccadar, @corrodedHash, @danielschemmel, @delcypher, @itbot08, @jasondavies, @jbuening, @jirislaby, @kren1, @Lysxia, @MartinNowack, @Mic92, @odeits-vidder, @SolalPirelli, @szeyiuchau, @Tipwheal, @yannicnoller)