about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
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-11Fixed and improved the stats on (cex)cache hits and misses.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@186097 91177308-0d34-0410-b5e6-96231b3b80d8
2013-05-08Patch by Dan Liew: "Renamed ExprSMTLIBPrinter method mangleQuery() to ↵Cristian Cadar
negateQueryExpression() to make it clear what it does." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@181445 91177308-0d34-0410-b5e6-96231b3b80d8
2013-04-05Fixed error that I introduced by mistake in the last commit (thanks again to ↵Cristian Cadar
Michael Contreras) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@178863 91177308-0d34-0410-b5e6-96231b3b80d8
2013-04-04Patch by Michael Contreras and Jiri Slaby for compiling KLEE with LLVM 3.2Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@178759 91177308-0d34-0410-b5e6-96231b3b80d8
2013-04-03Code reformatting.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@178642 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-27Patch by Jonathan Neuschäfer adding a missing newline.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@178168 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-18Patch and test case by Jiri Slaby to handle "initializing globals whenCristian Cadar
a global has an undef fill of holes inside structures." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@177285 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-11Forgot to add ConstructSolverChain.cpp in the previous patch.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176813 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-11Patch by Dan Liew which unifies the solver construction between KLEECristian Cadar
and Kleaver and fixes --use-query-log in Kleaver. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176811 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-06Patch by Tomek Kuchta which adds the --max-stp-time option to Kleaver.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176571 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-29Patch by Tomasz Kuchta that fixes the fragile way in which KLEE and Kleaver ↵Cristian Cadar
options were shared. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173819 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-22Added a new option --ignore-solver-failures, disabled by default, toCristian Cadar
cause KLEE to terminate on fatal solver errors. Better documented the ulimit issue when STP seg faults. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173187 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-22Patch by Hristina Palikareva which enables Kleaver to configure theCristian Cadar
solver chain. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173180 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Refactoring patch by Tomasz Kuchta that moves options shared by KLEE and ↵Cristian Cadar
Kleaver to a separate file. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171395 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Forgot to add QueryLoggingSolver in patch 171387 from Tomasz Kuchta.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171392 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Patch by Tomasz Kuchta adding more detailed information on query failures.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171391 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Patch by Tomasz Kuchta that refactors the logging code, by introducing a new ↵Cristian Cadar
logging class hierarchy. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171387 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Patch by Tomasz Kuchta adding a new option (min-query-time-to-log) that ↵Cristian Cadar
enables KLEE to log only the queries exceeding a certain duration, or only those that time out. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171385 91177308-0d34-0410-b5e6-96231b3b80d8
2012-11-28Only emitting a warning, instead of failing on large mallocs.Cristian Cadar
Addresses the issue raised by Bowen Zhou at http://keeda.stanford.edu/pipermail/klee-dev/2012-November/000972.html. Fixed test case that depended on the old behavior. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168797 91177308-0d34-0410-b5e6-96231b3b80d8
2012-11-27Warnings were incorrectly logged in messages.txt instead of warnings.txt.Cristian Cadar
Added "ONCE" before klee_warning_once messages to identify them as such. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168699 91177308-0d34-0410-b5e6-96231b3b80d8
2012-11-27Patch sent by both Bogdan Copos and Nick Sumner fixing compilation with LLVM 3.1Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168695 91177308-0d34-0410-b5e6-96231b3b80d8
2012-11-05Fixed a bug in Array::computeHash()Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@167382 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: "Added support for generating .smt2 files whenCristian Cadar
writing out test cases (option --write-smt2s) in KLEE." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166568 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew which improves the logging options: "RemovedCristian Cadar
-use-query-pc-log and -use-stp-query-pc-log and replaced with better command line option -use-query-log=option. Multiple comma seperated options can be specified after -use-query-log=. In addition queries can now be logged in SMT-LIBv2 format as well as KQuery format. The names of logging files has changed and also KLEE now informs users which files are being written to. Because of the changes the test/Feature/ExprLogging.c test broke so it was necessary to fix it." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166565 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: "Added SMTLIBLoggingSolver for logging queries in ↵Cristian Cadar
SMT-LIBv2 format." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166564 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Nice patch by Dan Liew that adds support for printing queries in theCristian Cadar
SMTLIB format (part of his MSc project work). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166556 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: "Moved PrintContext class out of ExprPrinter.cpp soCristian Cadar
it can be used by other classes. It has also been improved so it can be used with the soon to be added ExprSMTLIBPrinter classes." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166555 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: " Modified ConstantExpr::toString() to take anCristian Cadar
optional radix (base e.g. 2,10,16). This will be needed by the ExprSMTLIBPrinter that will soon be added." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166553 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-18Nice patch by Hristina Palikareva that removes the dependency on STPCristian Cadar
arrays from the Array and UpdateNode classes. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166214 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-08Fix to previous patch, which would not compile with LLVM 2.9.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@165413 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-08Make the changes in r165394 be conditional on post LLVM 3.1 changes.Micah Villmow
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@165405 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-08Move TargetData to DataLayout.Micah Villmow
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@165394 91177308-0d34-0410-b5e6-96231b3b80d8
2012-09-12Restructured the command-line options for setting the searchCristian Cadar
heuristics in KLEE. The new options are documented at http://klee.llvm.org/klee-options.html. Cleaned a bit the code in UserSearcher.cpp, and fixed some test cases to use the new options. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163711 91177308-0d34-0410-b5e6-96231b3b80d8
2012-09-11Changed the default to --max-memory and documented randomize-fork.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163632 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-31Patch by Dan Liew that removes our internal copy of STP, and makes the ↵Cristian Cadar
--with-stp option mandatory: "1. At configure time the --with-stp= option is now mandatory. 2. The HAVE_EXT_STP macro has been removed. 3. The ENABLE_EXT_STP autoconf replacement variable has been removed and consequently the Makefile variable of the same name has been removed." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161055 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-26Forgot a cl::desc in the previous patch...Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160781 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-26Documented several KLEE options.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160779 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-20Fixed bug FPToSI bug reported by Peng Li. Added a simple test case. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@160547 91177308-0d34-0410-b5e6-96231b3b80d8
2012-06-01Patch by Oscar Dustmann fixing a buffer overflow when long names areCristian Cadar
used: "patch for STPBuilder.cpp that allows for arbitrary length symbol names while still limiting the unique string to 32 bytes." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@157820 91177308-0d34-0410-b5e6-96231b3b80d8
2012-05-25Patch by Paul Marinescu that makes KLEE gracefully fail on assembly code.Cristian Cadar
Includes test case. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@157463 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-10Lowering support for the llvm.uadd.with.overflow intrinsic.Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154367 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-08Fixed --max-stp-time, which wasn't working unless --use-forked-stp wasCristian Cadar
also used. Thanks to Paul Marinescu for reporting and debugging this. The patch also disables the STP timeout by default. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154300 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-07Fix compilation with LLVM trunk.Peter Collingbourne
Patch by arrowdodger! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154238 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-07Catch up with hashing changes.Peter Collingbourne
Patch by arrowdodger! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154237 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-26STPBuilder: fix getShiftBits properly.Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@153475 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-26STPBuilder: fix bv{Zero,One,MinusOne} for the case where width>64Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@153474 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-26STPBuilder: fix ConstantExpr builder for the case where width>64 butPeter Collingbourne
is not a multiple of 64. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@153473 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-13Compatability fix for previous revision. By my mistake one string went out ↵Stepan Dyatkovskiy
of #if scobes. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@152625 91177308-0d34-0410-b5e6-96231b3b80d8