Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-08-27 | Remove unnecessary null pointer checks | Oscar Deits | |
Fixes klee/klee#717 delete on null pointer is always safe. | |||
2017-08-11 | Merge pull request #746 from ccadar/posix | Cristian Cadar | |
Fixed a bug causing KLEE to generate files with no permission bits, and added a basic test for klee-replay | |||
2017-08-10 | Added a basic test for klee-replay | Cristian Cadar | |
2017-08-09 | Fixed 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-09 | Merge pull request #745 from ccadar/misc | Andrea Mattavelli | |
Fixed a compiler warning (unused variable) | |||
2017-08-09 | Fixed a compiler warning (unused variable) | Cristian Cadar | |
2017-08-09 | Merge pull request #742 from ccadar/fold | Cristian Cadar | |
Added checks for div/mod by zero and overshifts in constant expressio… | |||
2017-08-07 | Untabify this file, which was using a mix of spaces and tabs for alignment. | Cristian Cadar | |
2017-08-07 | Added 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-04 | Removed merging searchers | Lukas Wölfer | |
2017-08-01 | Fixed 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-31 | Fix 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-29 | Added 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-29 | Added 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-28 | Merge pull request #728 from delcypher/cmake_change_default | Andrea Mattavelli | |
[CMake] Change some defaults | |||
2017-07-28 | Merge pull request #735 from andreamattavelli/fixes_travis_0717 | MartinNowack | |
[TravisCI] Some fixes for STP scripts | |||
2017-07-28 | Fixed script for STP in Travis-CI: Build now exits on errors | Andrea Mattavelli | |
2017-07-28 | Modified Travis-CI script to compile STP with BOOST support | Andrea Mattavelli | |
2017-07-28 | [TravisCI] Make sure when building with CMake that only the solvers | Dan Liew | |
requested get used. | |||
2017-07-28 | [CMake] Change the default value of `ENABLE_SOLVER_METASMT` to be set | Dan 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 uses | Dan 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 of | Dan 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 of | Dan Liew | |
`ENABLE_SOLVER_STP` to be set dynamically based on whether STP is available. Previously the default was always off. | |||
2017-07-27 | Merge pull request #734 from ccadar/misc | Cristian Cadar | |
Now that LLVM 2.9 is gone, we can use cl::bits when needed | |||
2017-07-26 | Now that LLVM 2.9 is gone, we can use cl::bits instead of cl::list | Cristian Cadar | |
2017-07-26 | Merge pull request #733 from ccadar/misc | Andrea Mattavelli | |
This reverts incorrect patch https://github.com/klee/klee/commit/db29… | |||
2017-07-26 | This reverts incorrect patch ↵ | Cristian Cadar | |
https://github.com/klee/klee/commit/db29a0bba74b672cdf4b8fef4d94ffa6ab845e6d __fprintf_chk has a different prototype than fprintf | |||
2017-07-25 | Added regression test for bug reported by @kren1 in #262 | Cristian Cadar | |
2017-07-25 | Merge pull request #726 from delcypher/cmake_fix_llvm_built_with_no_asserts | MartinNowack | |
[CMake] Handle building against LLVM built without assertions | |||
2017-07-25 | Cleanup tests for last LLVM 2.9 references | Andrea 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-25 | Merge pull request #725 from ccadar/fold | Cristian Cadar | |
Refactored some code related to constant evaluation | |||
2017-07-25 | [CMake] Fix bug where we would inherit LLVM's `-DNDEBUG` define | Dan Liew | |
when LLVM was built without assertions. This prevented `ENABLE_KLEE_ASSERTS` from working correctly. Reported by @MartinNowack . | |||
2017-07-25 | Merge pull request #724 from delcypher/floating_point_ops_clean_up | Andrea Mattavelli | |
Re-enable parts of `FloatingPointOps.ll` | |||
2017-07-25 | This commit simply moves evalConstant to ExecutorUtil (where ↵ | Cristian Cadar | |
evalConstantExpr also resides), as suggested by an old comment. | |||
2017-07-25 | Added the const qualifier to the keys in the constantMap | Cristian Cadar | |
2017-07-25 | Re-enable parts of `FloatingPointOps.ll`. The message about failures | Dan 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-24 | Moved klee_choose from klee-libc to KLEE intrinsics. | Cristian Cadar | |
2017-07-24 | more portable shebangs | Jö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-24 | llvm: get rid of static_casts from iterators (take 2) | Jörg Thalheim | |
follow up of c9c90a0ecdce10172fd5318aea60a9ff4057679f | |||
2017-07-24 | Merge pull request #721 from delcypher/cmake_runtime_dependency_fixes | Andrea Mattavelli | |
A few runtime build system fixes | |||
2017-07-24 | Merge pull request #713 from MartinNowack/remove_llvm_29_33 | Andrea Mattavelli | |
Remove support for LLVM < 3.4 | |||
2017-07-24 | [CMake] Add a sanity check to the runtime build system so that we | Dan 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 bitcode | Dan 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-23 | Remove LLVM 2.9 from Makefiles | Martin Nowack | |
2017-07-23 | Remove klee-gcc | Martin Nowack | |
2017-07-23 | Cleanup Travis builder | Martin Nowack | |
2017-07-23 | Updated test cases to reflect removal of LLVM 2.9 | Martin Nowack | |
2017-07-23 | Remove support for LLVM < 3.4 | Martin Nowack | |
Request LLVM 3.4 as minimal requirement for KLEE | |||
2017-07-21 | Release notes for 1.4.0 v1.4.0 1.4.x | Cristian Cadar | |