~cnx/klee - KLEE fork for patch differentiation testing

Age	Commit message (Collapse)	Author
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

2017-07-20	Switching version to 1.4.0	Cristian Cadar

2017-07-20	Merge pull request #657 from delcypher/vectorized_instructions	Cristian Cadar
	Implement basic support for vectorized instructions.
2017-07-20	Replace assertions of types on LLVM instructions in the Executor with a	Dan Liew
	pass that checks these assertions. This improves several things. * This pass provides more friendly messages than assertions in that it just emits a warning and carries on checking the rest of the instructions. * The takes the checks outside of the Executor's hot path and so avoids checking the same instruction multiple times. Now each instruction is only checked once just before execution starts. The disadvantage of this approach is the check for invariants we expect to hold have been pulled far away from where we expect them to hold. After discussion with @ccadar and @MartinNowack it was decided we will take this hit to readability for better performance and simpler code in the Executor.
2017-07-20	Merge pull request #673 from jirislaby/llvm40_WallTimer	MartinNowack
	Core: TimingSolver, use WallTimer