about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2017-08-27Remove unnecessary null pointer checksOscar Deits
Fixes klee/klee#717 delete on null pointer is always safe.
2017-08-11Merge pull request #746 from ccadar/posixCristian Cadar
Fixed a bug causing KLEE to generate files with no permission bits, and added a basic test for klee-replay
2017-08-10Added a basic test for klee-replayCristian Cadar
2017-08-09Fixed a bug causing KLEE to generate files with no permissions bits set. ↵Cristian Cadar
This was introduced when we added the --readable-posix-inputs option.
2017-08-09Merge pull request #745 from ccadar/miscAndrea Mattavelli
Fixed a compiler warning (unused variable)
2017-08-09Fixed a compiler warning (unused variable)Cristian Cadar
2017-08-09Merge pull request #742 from ccadar/foldCristian Cadar
Added checks for div/mod by zero and overshifts in constant expressio…
2017-08-07Untabify this file, which was using a mix of spaces and tabs for alignment.Cristian Cadar
2017-08-07Added checks for div/mod by zero and overshifts in constant expressions. ↵Cristian Cadar
Such div/mod by zero expressions would previously crash KLEE. Added two test cases, one for div/mod by zero, the other for overshift. This fixes the bug reported in #268.
2017-08-04Removed merging searchersLukas Wölfer
2017-08-01Fixed test case counter: Previously the number of test cases generated by ↵Andrea Mattavelli
KLEE was always incremented, even if a symbolic solution was not found.
2017-07-31Fix build for FreeBSD.Tatiana Tikhomirova
On FreeBSD <sys/capabilities.h> is present in libc, so we don't require libcap there. Close and write functions are located in <unistd.h>.
2017-07-29Added an optional KInstruction* argument to evalConstant and ↵Cristian Cadar
evalConstantExpr which allows us to print the location associated with the constant in any error messages. Added a test case for the unsupported features for taking the address of a label, which exercises the patch.
2017-07-29Added another variant of printFileLine in KInstruction that returns the ↵Cristian Cadar
location as a string. Also added const qualifier to the printFileLine functions
2017-07-28Merge pull request #728 from delcypher/cmake_change_defaultAndrea Mattavelli
[CMake] Change some defaults
2017-07-28Merge pull request #735 from andreamattavelli/fixes_travis_0717MartinNowack
[TravisCI] Some fixes for STP scripts
2017-07-28Fixed script for STP in Travis-CI: Build now exits on errorsAndrea Mattavelli
2017-07-28Modified Travis-CI script to compile STP with BOOST supportAndrea Mattavelli
2017-07-28[TravisCI] Make sure when building with CMake that only the solversDan Liew
requested get used.
2017-07-28[CMake] Change the default value of `ENABLE_SOLVER_METASMT` to be setDan Liew
dynamically based on whether MetaSMT is available. Previously the default was always off.
2017-07-28[CMake] Add `ENABLE_ZLIB` option to control whether KLEE usesDan Liew
zlib. The default is `ON` if zlib is found on first configure and `OFF` if zlib is not found on first configure.
2017-07-28[CMake] Refactor Z3 detection and change the default value ofDan Liew
`ENABLE_SOLVER_Z3` to be set dynamically based on whether Z3 is available. Previously the default was always off.
2017-07-28[CMake] Refactor STP detection and change the default value ofDan Liew
`ENABLE_SOLVER_STP` to be set dynamically based on whether STP is available. Previously the default was always off.
2017-07-27Merge pull request #734 from ccadar/miscCristian Cadar
Now that LLVM 2.9 is gone, we can use cl::bits when needed
2017-07-26Now that LLVM 2.9 is gone, we can use cl::bits instead of cl::listCristian Cadar
2017-07-26Merge pull request #733 from ccadar/miscAndrea Mattavelli
This reverts incorrect patch https://github.com/klee/klee/commit/db29…
2017-07-26This reverts incorrect patch ↵Cristian Cadar
https://github.com/klee/klee/commit/db29a0bba74b672cdf4b8fef4d94ffa6ab845e6d __fprintf_chk has a different prototype than fprintf
2017-07-25Added regression test for bug reported by @kren1 in #262Cristian Cadar
2017-07-25Merge pull request #726 from delcypher/cmake_fix_llvm_built_with_no_assertsMartinNowack
[CMake] Handle building against LLVM built without assertions
2017-07-25Cleanup tests for last LLVM 2.9 referencesAndrea Mattavelli
2017-07-25[CMake] Emit warning when mixing assert and non assert builds.Dan Liew
This could lead to lots of problems. If we discover that these configurations don't work at all we should make this an error.
2017-07-25Merge pull request #725 from ccadar/foldCristian Cadar
Refactored some code related to constant evaluation
2017-07-25[CMake] Fix bug where we would inherit LLVM's `-DNDEBUG` defineDan Liew
when LLVM was built without assertions. This prevented `ENABLE_KLEE_ASSERTS` from working correctly. Reported by @MartinNowack .
2017-07-25Merge pull request #724 from delcypher/floating_point_ops_clean_upAndrea Mattavelli
Re-enable parts of `FloatingPointOps.ll`
2017-07-25This commit simply moves evalConstant to ExecutorUtil (where ↵Cristian Cadar
evalConstantExpr also resides), as suggested by an old comment.
2017-07-25Added the const qualifier to the keys in the constantMapCristian Cadar
2017-07-25Re-enable parts of `FloatingPointOps.ll`. The message about failuresDan Liew
doesn't seem relevant anymore given that LLVM 3.4 is the minimum version KLEE supports. Also do minor clean up. This was spotted by @andreamattavelli.
2017-07-24Moved klee_choose from klee-libc to KLEE intrinsics.Cristian Cadar
2017-07-24more portable shebangsJörg Thalheim
This is useful on systems like NixOS, where python3 is not in /usr/bin/python3 as well as for people using alternative ways to install python such as virtualenv/pyenv. Some scripts where already using '/usr/bin/env'. With this pull request it gets more consistent. For background information see also: https://github.com/systemd/systemd/pull/5816
2017-07-24llvm: get rid of static_casts from iterators (take 2)Jörg Thalheim
follow up of c9c90a0ecdce10172fd5318aea60a9ff4057679f
2017-07-24Merge pull request #721 from delcypher/cmake_runtime_dependency_fixesAndrea Mattavelli
A few runtime build system fixes
2017-07-24Merge pull request #713 from MartinNowack/remove_llvm_29_33Andrea Mattavelli
Remove support for LLVM < 3.4
2017-07-24[CMake] Add a sanity check to the runtime build system so that weDan Liew
provide a better error message (and stop earlier) when no C source files are found.
2017-07-24[CMake] Fix bug where the runtime build system would not rebuild bitcodeDan Liew
archive/modules when the list of source files that constitute it changes. To fix this a file is written in the build directory that contains the list of `.bc` files. This file is updated whenever the list of `.bc` files for a module changes and then the rule that builds the module/archive depends on that file. This fixes a bug reported by @ccadar in #718.
2017-07-23Remove LLVM 2.9 from MakefilesMartin Nowack
2017-07-23Remove klee-gccMartin Nowack
2017-07-23Cleanup Travis builderMartin Nowack
2017-07-23Updated test cases to reflect removal of LLVM 2.9Martin Nowack
2017-07-23Remove support for LLVM < 3.4Martin Nowack
Request LLVM 3.4 as minimal requirement for KLEE
2017-07-21Release notes for 1.4.0 v1.4.0 1.4.xCristian Cadar