~cnx/klee - KLEE fork for patch differentiation testing

Age	Commit message (Collapse)	Author
2015-04-18	Merge pull request #213 from MartinNowack/klee-clang	Cristian Cadar
	Add klee-clang as alternative to klee-gcc
2015-04-15	Add clang-format style. We just use LLVM's style.	Dan Liew

2015-04-15	Fix the handling of AShrExpr in ExprSMTLIBPrinter so that an overshift	Dan Liew
	always goes to zero (matches LLVM's APInt::ashr(...)). This is meant to partially address issue #218. There are a few problems with this commit * It is possible for AShrExpr to not be abbreviated because the scan methods will not see that we print the 0th child of the AShrExpr twice * The added test case should really be run through an SMT solver ( i.e. STP) but that requires infrastructure changes.
2015-04-10	The Docker image had python2 and python3 which is a waste of space	Dan Liew
	(I'm not sure where python3 came from. I didn't explicitly install it). Just ship python3.
2015-04-10	Don't upgrade pip or setuptools. Upgrading pip breaks the build because	Dan Liew
	/usr/local/bin/ isn't in PATH so using pip after upgrading it fails.
2015-04-10	Add missing slash in last commit.	Dan Liew

2015-04-10	Update Dockerfile	David Leon Gil
	klee-stats requires tabulate to be installed.
2015-04-09	Add initial Dockerfile for building a KLEE Docker image (uses LLVM3.4).	Dan Liew
	This is is tightly coupled with the TravisCI scripts. There are some really nasty hacks in here that we should get rid of at some point.
2015-04-09	Try to fix using the compiler KLEE's configure script detected again!	Dan Liew
	My first attempt in b41cf33b6b726fd97e502c5c4818f5feeea0284b was wrong because setting the CC and CXX Makefile variables in Makefile.config.in did not work because LLVM's Makefile.config would override them. Also detecting the C compiler is unnecessary because we already do this (bitcode compiler detection)
2015-04-09	Normalised line endings	Cristian Cadar

2015-04-09	Added .gitattribute file that takes care of line endings.	Cristian Cadar

2015-04-09	Fix mistake if TravisCI scripts where configure flag for enabling POSIX	Dan Liew
	runtime was incorrect.
2015-04-09	Added a new option, --rewrite-equalities, which makes it possible to disable ↵	Cristian Cadar
	the optimisation that rewrites existing constraints when an equality with a constant is added
2015-04-09	Switch to using STP's fork of minisat for TravisCI. It contains fixes	Dan Liew
	needed by Clang.
2015-04-08	Fix very annoying issue where KLEE's configure would completly	Dan Liew
	ignore the C++ compiler detected and just use the compiler detected during the LLVM configure.
2015-04-03	Upstream STP now depends on an external build of minisat. Attempt to	Dan Liew
	fix travis build of upstream STP and also how KLEE links against STP.
2015-04-03	Fixed issue introduce during a previous refactoring, related to field ordering.	Cristian Cadar

2015-04-02	Use C instead of C++ comments in C files to silence compiler warnings.	Cristian Cadar

2015-04-02	Silenced some compilation warnings.	Cristian Cadar

2015-04-02	Merge pull request #209 from erakadjiev/timestamp_optimize	Cristian Cadar
	Cleaner, more efficient timestamps
2015-04-02	Revert "[include] Added documentation" to avoid a conflict with a pending ↵	Cristian Cadar
	pull request. This reverts commit badffc570e1be6b675dcab7e21829bd029c46287.
2015-04-02	Fixed some doxygen issues.	Cristian Cadar

2015-04-02	Removed unused fakeState field from ExecutionState	Cristian Cadar

2015-04-02	Pass over the comments in ExecutionState.h	Cristian Cadar

2015-04-02	Removed underConstrained field, which I believe was re-introduced by	Cristian Cadar
	mistake in the last cleanup commit.
2015-04-02	[Core] Documentation and cleanup	Martin Nowack
	* Removed unused member ShadowObjects in ExecutionState * Added documentation of members and reorder according to categories
2015-04-01	[include] Add missing functions in klee.h	Martin Nowack

2015-04-01	[runtime] Fix include in klee_int	Martin Nowack

2015-04-01	[test] Fix compilation warning	Martin Nowack
	Use correct definition and declaration of main function
2015-04-01	[Core] Fixed typo in assertion	Martin Nowack

2015-04-01	[runtime] Fix comments to c style for c files and headers	Martin Nowack

2015-04-01	[tests] Fix undefined function	Martin Nowack
	Add some missing header to silence compiler warnings
2015-04-01	[tools] Added fortified version wrapper for fprintf	Martin Nowack

2015-04-01	[include] Added documentation	Martin Nowack

2015-04-01	[include] Removed unused variable	Martin Nowack

2015-03-22	Fix compilation under MacOS, see https://github.com/klee/klee/issues/219 for ↵	Cristian Cadar
	details.
2015-03-20	Improve arithmetic-right-overshift-sym-conc.c test by make sure it	Dan Liew
	also test a negative constant as the lhs.
2015-03-20	[Solver] Fix leak intermediate expression not freed	Martin Nowack

2015-03-20	[Core] Fix memory leak in assembler raising	Martin Nowack

2015-03-13	Timestamp improvements.	Emil Rakadjiev
	Replaced inefficient llvm::sys::Process::GetTimeUsage() with TimeValue::now(), because in many cases only the wall clock time is needed, not the user and sys times (which are significantly more expensive to get). Updated TimingSolver and WallTimer accordingly.
2015-03-12	Merge pull request #212 from MartinNowack/killing_states_warning	Cristian Cadar
	[Core] Always warn if states get deleted due to memory limits
2015-03-12	[Core] Always warn if states get deleted due to memory limits	Martin Nowack

2015-03-12	Add klee-clang as alternative to klee-gcc	Martin Nowack

2015-03-03	Consistent capitalization of "KLEE"	Cristian Cadar

2015-03-03	Slight updates in license file, acknowledging more recent contributions.	Cristian Cadar

2015-03-02	New regression test checking that the Array factory correctly distinguishes ↵	Cristian Cadar
	between arrays created at the same location but with different sizes
2015-03-02	Merge branch 'holycrap872-ArrayFactory'	Cristian Cadar

2015-02-27	Improved some comments and fixed some formatting issues in the Array factory ↵	Cristian Cadar
	patch.
2015-02-27	Merge branch 'ArrayFactory' of https://github.com/holycrap872/klee into ↵	Cristian Cadar
	holycrap872-ArrayFactory
2015-02-22	Added factory method for Arrays + hid constructors from outside calls	Eric Rizzi
	The way that Arrays were handled in the past led to the possibility of aliasing issues. This occured whenever a new branch discovered an array for the first time. Each branch would create a new instance of the same array without seeing if it had been created before. Therefore, should a new branch encounter the same state as some previous branch, the previous branch's solution wouldn't satisfy the new state since they didn't recognize they were referencing the same array. By creating an array factory that creates a single symbolic array, that problem is handled. Note: Concrete arrays should not be created by the factory method since their values are never shared between branches. The factory works by seeing if an array with a similar hash has been created before (the hash is based on the name and size of array). If there has been it then searches through all of the arrays with the same hash (stored in a vector) to see if there is one with an exact match. If there is one, the address of this previously created equivalent array is returned. Otherwise, the newly created array is unique, it is added to the map, and it's address is returned. This aliasing issue can be seen by comparing the output of the Dogfood/ImmutableSet.cpp test cases with and with out this commit. Both act correctly, but the number of queries making it to the solver in the previous version is much greater 244 vs 211. This is because the UBTree in the CexCachingSolver and the cache in the CachingSolver do not recognize queries whose solutions were previously calculated because it doesn't think the arrays in the two queries are the same. While this does not cause an error, it does mean that extra calls are made.