about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Collapse)Author
2010-05-24Removed unused use-query-log option, patch submitted by Peter Collingbourne.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@104487 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Fix a Wformat warning.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102877 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Add missing include of Config.h, which was causing LLVM version checks to beDaniel Dunbar
broken, and thus we were removing all dbg.stoppoint instructions from modules. This totally broke debug info with 2.6. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102873 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Fix some const cast warnings.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102867 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-26Applied patch submitted by Peter Collingbourne: "Some parts of theCristian Cadar
KLEE source code do not conform to the C++ standard, specifically [basic.scope.local]. gcc accepts the code due to a bug [1] but some other compilers (e.g. those based on EDG, such as icc) do not. This patch fixes the code in question to conform to the standard. [1] http://gcc.gnu.org/bugzilla/show_bug.cgi?id=18770" git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102328 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-22Added --stp-optimize-divides flag. Patch submitted by PeterCristian Cadar
Collingbourne: "This flag controls whether constant divides are optimized into add/shift/multiplies before passing to STP, and is set by default. In some circumstances the use of this optimisation can actually slow the solver down, so it is best to allow the user to disable it." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102069 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-22Applied patch submitted by Peter Collingbourne: "If either of theseCristian Cadar
values is 0, the overall STP timeout should be whichever of the two values is set, i.e. the maximum of the 2 values, rather than 0." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102058 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05Add long double support, patch by David Ramos.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100421 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05Make sure to include config.h, for llvm version check.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100398 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05STP: Switch build to using LLVM style Makefiles.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100395 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05Update for LLVM API change.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100383 91177308-0d34-0410-b5e6-96231b3b80d8
2010-03-14Update for 2.7.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@98467 91177308-0d34-0410-b5e6-96231b3b80d8
2010-03-14Kill off ExecutionTrace stuff, it is too messy.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@98466 91177308-0d34-0410-b5e6-96231b3b80d8
2010-02-25Applied patch submitted by Justin Lebar to fix compilation error w/Cristian Cadar
gcc 4.4. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@97153 91177308-0d34-0410-b5e6-96231b3b80d8
2010-02-09Fix PR6211, the comparison was created with the wrong width. Patch by StefanDaniel Dunbar
Bucur! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@95659 91177308-0d34-0410-b5e6-96231b3b80d8
2009-10-25Update source to build against LLVM 2.6Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@85024 91177308-0d34-0410-b5e6-96231b3b80d8
2009-09-21Improve skipping of debug intrinsics, we can't evaluate MDNode operands.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@82421 91177308-0d34-0410-b5e6-96231b3b80d8
2009-09-21Don't try to evaluate MDNode operands.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@82420 91177308-0d34-0410-b5e6-96231b3b80d8
2009-09-05Applied patch submitted by Pongsin Poosankam that fixes a bug in theCristian Cadar
parser. Fixed bug in the parses. Patch reported by git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@81056 91177308-0d34-0410-b5e6-96231b3b80d8
2009-09-01Update for LLVM ostream changes.Daniel Dunbar
- Includes patch by Michael Stone! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@80665 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-24Applied the patch submitted by Robby Cochran that fixes an arithmetic ↵Cristian Cadar
overflow in Solver::getRange(). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@79945 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-17Update for LLVM API change.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@79217 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-03Fix computation of GetElementPtr offset for 64-bit targets.Daniel Dunbar
- Precomputed constants were being truncated to 32-bits! - This was actually the problem with new[]/delete[], I failed to look at the generated code for new[] to realize that the compiler is generating the offset pointer, not the runtime library. - All tests now pass on x86-64! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77930 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-02Print allocation info for adjacent objects in out-of-bounds message.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77922 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-01Implement va_arg handling for x86_64.Daniel Dunbar
- Based on a patch by Vladimir Kuznetsov! - x86_64 has a complicated calling convention for va_args; instead of dealing with this, this patch uses a clever workaround by initializing the va_list structure so that the callee believes all arguments were passed in the stack save area. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77819 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-01KLEE64: Fix initialization of ctype_ externals.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77816 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-01Add Expr::dumpDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77802 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-01When generating external function stubs, access the arguments in terms of theDaniel Dunbar
function type, not the argument types. This accomodates for a conversion which is done in Executor.cpp. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77801 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-01Rename intrinsic library to libkleeRuntimeInstrinsic, for consistency.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77797 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-01Avoid failing if waitpid fails with EINTR, patch by Vladimir Kuznetsov.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77770 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-29Multiply for alloca & malloca instructions may need to coerce index expressionDaniel Dunbar
to target pointer width. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77428 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-28Add missing va_end and null check.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77312 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-28KLEE64: Fix a type conversion problem with calls to klee_make_symbolic; thereDaniel Dunbar
are probably lots more of this -- we really need coercion and argument validation to be checked outside of the individual intrinsic handlers. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77311 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-28KLEE64: When binding GetElementPtr constants, do evaluation in pointer width ofDaniel Dunbar
target. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77310 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-28KLEE64: Regardless of the target, offsets in the memory subsystem are 32-bits. IDaniel Dunbar
don't think anyone is going to be doing symbolic execution with > 4GB buffers any time soon, and this is slightly simpler. - We know pass about half of KLEE's test suite on Darwin x86_64. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77309 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-28KLEE64: GetElementPtr constants should be evaluated in the target pointer width.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77308 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-28KLEE64: Fix some totally bogus printing code, which was reusing a va_listDaniel Dunbar
without va_copy()ing it. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77307 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-28Move Machine constants into Context object, initialized based on the targetDaniel Dunbar
data. - This is the first step towards having KLEE be fully target independent, its not particularly beautiful but its expedient. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77306 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-25(llvm up) Update for llvm::Value getName() change.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77049 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-25(llvm up) Update for API changes.Daniel Dunbar
- This dance is getting old. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77029 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-17Simplify some code, and add more comments.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@76152 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-17Add some comments for CexCachingSolver::searchForAssignment.Daniel Dunbar
- No functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@76148 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-15[llvm up] Update for LLVM TOT changes.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75826 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-15Code to answer satisfiability queries.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75735 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-12Update for LLVM API changes.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75427 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-12Simplify.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75425 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-11Removed the Nz macro.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75377 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-11Use a builder in the SMT parser instead of constructing expressionsCristian Cadar
directly. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75323 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-11Report an error in the SMT parser when encountering the few operatorsCristian Cadar
not supported yet: bvneg, bvsmod, bvxnor, rotate_left, rotate_right, repeat. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75319 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Removed debug info.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75313 91177308-0d34-0410-b5e6-96231b3b80d8