about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2013-09-02Implemented runtime check for overshift (controllable with --check-overshiftDan Liew
command line argument). Overshift is where a Shl, AShr or LShr has a shift width greater than the bit width of the first operand. This is undefined behaviour in LLVM so we report this as an error.
2013-09-02Fixed bug where divide by zero bugs would only be detected once in a programDan Liew
even if there were many divide by zero bugs. The fix basically inlines all function calls to klee_div_zero_check() so that each call to klee_report_error() is a unique instruction for each instrumentation of a divide operation. It also seems that inlining the call "magically" fixed the debug information (file and line number) of the instruction so that the debug information on the inlined instructions matches that of the instrumented division instruction. Note that the command line option -emit-all-errors could be used to workaround the bug fixed in this commit.
2013-08-30Merge branch 'CompilerWarnings' of https://github.com/MartinNowack/klee into ↵Cristian Cadar
MartinNowack-CompilerWarnings
2013-08-29Revert "Use new PathV2 interface for LLVM 2.9 and higher"Martin Nowack
This reverts commit 5c059018c02a7c7db252a3cb636a39c89c430a06.
2013-08-29Merge branch 'CompilerWarnings' of https://github.com/MartinNowack/klee into ↵Cristian Cadar
MartinNowack-CompilerWarnings
2013-08-29Fix compiling issues with llvm 2.9Martin Nowack
Interface for ParseCommandLineOptions changed with LLVM 3.2 preserving constness for pointer to arguments.
2013-08-29Use new PathV2 interface for LLVM 2.9 and higherMartin Nowack
Enable PathV2 interface starting from LLVM 2.9 and do some minor include cleanup.
2013-08-28Merge branch 'CompilerWarnings' of https://github.com/MartinNowack/klee into ↵Cristian Cadar
MartinNowack-CompilerWarnings
2013-08-28Merge pull request #22 from antiAgainst/masterCristian Cadar
Add .gitignore
2013-08-28Merge pull request #13 from MartinNowack/FeatureConstantArraysCristian Cadar
Patch Set IV - Handle constant arrays as well
2013-08-28Fixed warning about unused variableMartin Nowack
2013-08-28Fix constness warnings issued by gcc 4.7Martin Nowack
2013-08-28Link against shared library from LLVM correctlyMartin Nowack
Searching for the LLVM library was conducted in the Klee project. This patch searches in the LLVM build directory.
2013-08-28Silence warning of deprecated PathV1 usageMartin Nowack
2013-08-28Fix test case to use llvm-link instead of llvm-ldMartin Nowack
2013-08-28Disable redefinition of functionsMartin Nowack
2013-08-28Silence compiler warning about unused variableMartin Nowack
2013-08-27Handle constant arrays as wellMartin Nowack
2013-08-26Add Debug and Debug+Asserts in .gitignore.Lei Zhang
2013-08-26Add .gitignoreLei Zhang
2013-08-16Merge pull request #9 from delcypher/refactor-arg-initCristian Cadar
Slight refactor of code initialising memory for argments/environment c-strings
2013-08-15Merge pull request #14 from MartinNowack/BuildSystemCristian Cadar
Patch Set V - Build system
2013-08-15Add support for dejagnu as removed from LLVM 3.2Martin Nowack
Added support for dejagnu to still allow tests to be executed under LLVM 3.2.
2013-08-15Use llvm-link instead of deprecated llvm-ldMartin Nowack
2013-08-15Warn if compiler is not found to build .ll filesMartin Nowack
2013-08-15Merge pull request #18 from MartinNowack/FeatureUMulOverflowCristian Cadar
Patch Set III (update) Implemented llvm.umul.with.overflow
2013-08-15Implemented llvm.umul.with.overflowMartin Nowack
2013-08-15Merge pull request #16 from MartinNowack/DebugSymbolsCristian Cadar
Patch Set VII - Handle additional debug intrinsics of LLVM
2013-08-15Merge pull request #10 from MartinNowack/TyposCristian Cadar
Fixed typos.
2013-08-14Handle additional debug intrinsics of LLVMMartin Nowack
2013-08-14Fix typoMartin Nowack
2013-08-14Fix typoMartin Nowack
2013-08-14Slight refactor of code initialising memory for argments/environment c-stringsDan Liew
so that it is easier to read.
2013-08-13Modified ktest-tool so that it is compatible with python3.Dan Liew
2013-08-13Updated configure.ac to use python3 compatible command.Dan Liew
2013-08-07Merge branch 'master' of https://github.com/hpalikareva/klee into ↵Cristian Cadar
hpalikareva-master
2013-08-07Merge branch 'bfs' of https://github.com/antiAgainst/klee into antiAgainst-bfsCristian Cadar
2013-08-06ObjectState::concreteStore initialised.Hristina Palikareva
2013-08-06TimingSolver and constructSolverChain() no longer coupled with pointers to ↵Hristina Palikareva
STPSolver objects. Timeout is now set by the solver at the top of the solver chain rather than by STPSolver.
2013-08-06Methods getConstraintLog() and setTimeout() made virtual and moved from ↵Hristina Palikareva
STPSolver to base Solver and SolverImpl classes, and consequently redefined in derived classes to call the corresponding methods down the solver chain. Method setTimeout() renamed to setCoreSolverTimeout().
2013-08-06Renaming solver-related command-line options in order to decouple them from ↵Hristina Palikareva
STP. More specifically, command-line options max-stp-time, use-forked-stp and stp-optimize-divides renamed to max-solver-time, use-forked-solver and solver-optimize-divides, respectively. Option of running the SMT solver in a separate process (i.e. forked) set to true by default. Options of running SMT solver forked and with optimized divides made available to Kleaver as well.
2013-07-26Merge pull request #1 from ddcc/masterccadar
Remove website from master tree
2013-07-25remove www from master branchDominic Chen
2013-07-25Revert "move website to separate repo"Dominic Chen
This reverts commit 6ae711b1d900bffbca407fe97d5e5ce97745dff1.
2013-07-25move website to separate repoDominic Chen
2013-07-23BFS searcher.Lei Zhang
2013-07-19Paper on redundant state detection.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@186669 91177308-0d34-0410-b5e6-96231b3b80d8
2013-07-18Patch by Stephan Falke fixing an incorrect message. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@186589 91177308-0d34-0410-b5e6-96231b3b80d8
2013-07-11Bug fix by Jonathan Neuschäfer: "Without this patchCristian Cadar
NotExpr::computeHash() will have a local variable with the name "hashValue" and assign the newly computed hash to that instead of the member variable with the same name that should be set by the computeHash method of every Expr subclass." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@186102 91177308-0d34-0410-b5e6-96231b3b80d8
2013-07-11Patch by Jonathan Neuschäfer to LICENSE.TXT: "STP has been removed from the ↵Cristian Cadar
KLEE repository in r161056." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@186100 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-19 07:38:41 +0000