about summary refs log tree commit diff homepage
path: root/lib/Core
AgeCommit message (Collapse)Author
2013-10-11MetaSMT builder, solver and command-line options.Hristina Palikareva
2013-09-25Merge pull request #25 from paulmar/masterCristian Cadar
Added some of the common *at functions & others to the model. Obey --max-forks in switch statements.
2013-09-25Obey --max-forks in switch statementsPaul Marinescu
2013-09-21Merge pull request #17 from MartinNowack/LLVM33Cristian Cadar
Make KLEE compile with LLVM 2.3.
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-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-28Fix constness warnings issued by gcc 4.7Martin Nowack
2013-08-28Silence warning of deprecated PathV1 usageMartin Nowack
2013-08-27Handle constant arrays as wellMartin Nowack
2013-08-27Port to LLVM 3.3Martin Nowack
Major changes are: - Switching to llvm-link to build archive files - Use GetMallocUsage instead of GetTotalMemoryUsage (be aware of bug in LLVM 3.3 http://llvm.org/bugs/show_bug.cgi?id=16847) - intrinsic library functions like memcpy/mov/set use weak linkage to be replaced by e.g. uclibc functions - rewrote linking with library - enhanced MemoryLimit test case to check if mallocs were successful
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-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-07Merge branch 'master' of https://github.com/hpalikareva/klee into ↵Cristian Cadar
hpalikareva-master
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-23BFS searcher.Lei Zhang
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-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-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-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-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-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-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-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-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-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-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-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
2012-03-11llvm::SwitchInstStepan Dyatkovskiy
Renamed methods caseBegin, caseEnd and caseDefault with case_begin, case_end, and case_default. Added some notes relative to case iterators. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@152534 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-08Taken into account Duncan's comments for r149481 dated by 2nd Feb 2012:Stepan Dyatkovskiy
http://lists.cs.uiuc.edu/pipermail/llvm-commits/Week-of-Mon-20120130/136146.html Implemented CaseIterator and it solves almost all described issues: we don't need to mix operand/case/successor indexing anymore. Base iterator class is implemented as a template since it may be initialized either from "const SwitchInst*" or from "SwitchInst*". ConstCaseIt is just a read-only iterator. CaseIt is read-write iterator; it allows to change case successor and case value. Usage of iterator allows totally remove resolveXXXX methods. All indexing convertions done automatically inside the iterator's getters. Main way of iterator usage looks like this: SwitchInst *SI = ... // intialize it somehow for (SwitchInst::CaseIt i = SI->caseBegin(), e = SI->caseEnd(); i != e; ++i) { BasicBlock *BB = i.getCaseSuccessor(); ConstantInt *V = i.getCaseValue(); // Do something. } If you want to convert case number to TerminatorInst successor index, just use getSuccessorIndex iterator's method. If you want initialize iterator from TerminatorInst successor index, use CaseIt::fromSuccessorIndex(...) method. There are also related changes in llvm-clients: klee and clang. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@152299 91177308-0d34-0410-b5e6-96231b3b80d8
2012-02-12Teach KLEE how to handle new ConstantDataSequential type.Peter Collingbourne
Patch by arrowdodger! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@150355 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-06-05 19:32:35 +0000