~cnx/klee - KLEE fork for patch differentiation testing

Age	Commit message (Collapse)	Author
2014-02-14	Fixed overshift of arithmetic right shift by constant so that it	Dan Liew
	overshifts to zero. Test case is included.
2014-02-14	Fixed overshift of arithmetic right shift by symbolic so that it overshifts	Dan Liew
	to zero. Test case is included.
2014-02-14	Fixed overshift of logical right shift by constant so that it	Dan Liew
	overshifts to zero. Test case is included.
2014-02-14	Fixed overshift of logical right shift by symbolic so that it overshifts	Dan Liew
	to zero. Test case is included.
2014-02-14	Fixed overshifting an expression by a constant so that we overshift to	Dan Liew
	zero. A test case was added for this. In addition the use to vc_bvExtract() was removed for shifting left by an expression because we don't want/need bitmasked behaviour anymore.
2014-02-14	Added a test case for testing overshift behaviour of Shl and fixed	Dan Liew
	a bug in the previous commit where 32-bit width was assumed.
2014-01-20	Remove the last remnants (I think) of DejaGNU. Goodbye!	Dan Liew
	Say hello to our new friend, llvm-lit :)
2014-01-20	Fixed many tests that make use of the file tool to check	Dan Liew
	a file created by KLEE exists. A big difference between DejaGNU and llvm-lit is that in DejaGNU the working directory is the test output directory (e.g. test/Feature/Output) but in llvm-lit the working directory is the test directory (e.g. test/Feature ) To fix this I have used the %T substitution variable for llvm-lit. I have also improved some tests by using LLVM's FileCheck tool and removing of hard coded constants for data type size in some places. This commit inevitably breaks running the tests under DejaGNU. Although it is possible to hack by introducing the %T substitution variable some tests would still be broken because the use of shell pipes in DejaGNU doesn't seem to work properly. I could work around this but it's really not worth the effort.
2013-10-15	Fixed nondeterministic behaviour in test case ./test/Solver/LargeIntegers.pc ↵	Hristina Palikareva
	-- only 16 bytes of array a were initialised in Query 2, but values of 17 bytes were later required for comparison.
2011-07-24	Applied patch by Leandro Sales that makes Kleaver compatible with the	Cristian Cadar
	recent changes to array names. Modified FastCexSolver.pc to catch this issue. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135896 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-26	More large integer support.	Daniel Dunbar
	- Allow constructing a ConstantExpr from an APInt, too painful otherwise. - Parser support for large integers. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74278 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25	Kill off last getConstantValue uses.	Daniel Dunbar
	- ConstantExpr should now fully support arbitrary width operations. - Still numerous holes in parsing, solver, etc. to plug. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74151 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16	Improve FastCexSolver:	Daniel Dunbar
	- Bug fix, unbreak Concat propogation (recent regression). - Also, add some simple propogation for Add. - These two knock off another 50% of the queries hitting STP from the first 30s of 'dd'. - Also, add some debugging code. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73488 91177308-0d34-0410-b5e6-96231b3b80d8