about summary refs log tree commit diff homepage
path: root/include
AgeCommit message (Collapse)Author
2010-08-05Have getDirectCallTarget use CallSitePeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@110351 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-15Fix some -Wmismatched-tags warnings.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108403 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-15Remove stray semicolons in class definitions.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108402 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-14Add option to use an external version of STPPeter Collingbourne
This patch adds a new configure option, --with-stp, which configures KLEE to use an external version of STP instead of the version in the source tree. It includes documentation referring users to the STP download location. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108347 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-08Add support for InsertValue and ExtractValue instructionsPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107912 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-28Applied Stefan Bucur's patch fromCristian Cadar
http://llvm.org/bugs/show_bug.cgi?id=6690. The patch adds specialized versions of klee_get_value for different types, fixing the previous klee_get_value function that sometimes truncated 64bit parameters to 32bit. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107006 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-24Use LLVM's TargetData::getTypeSizeInBits to determine type bitwidth instead ↵Peter Collingbourne
of our own implementation git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106800 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-24Implement klee_stack_trace functionPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106799 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-24Added ExecutionState::dumpStack function for inspecting the status of the stackPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106798 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-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-05Fix some final objdir != src problems.Daniel Dunbar
- PR4269. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100396 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-13Fix some doxyments, patch by Peter Collingbourne!Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@96101 91177308-0d34-0410-b5e6-96231b3b80d8
2009-10-24Regenerate configure.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@85023 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-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-01Add Expr::dumpDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77802 91177308-0d34-0410-b5e6-96231b3b80d8
2009-08-01Use size_t where appropriate for ImmutableTree and friends.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77799 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-10Added support for bitwise not. Replacing "false == " with Not inCristian Cadar
the canonical form. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75239 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Replaced createNot() by createIsZero() and "Not" macro by "Nz". Cristian Cadar
Not will become bitwise not. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75224 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-27Start move to using APFloat (support long double).Daniel Dunbar
- Incomplete, still have to move some conversion operations. - Also, there isn't support yet for copying long double values to native memory. - Still, should be a monotonic improvement and we are no longer faking long double support. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74363 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-26More 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-25Kill 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-25Remove some more uses of getConstantValue.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74149 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Switch to using APInt math operations.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74148 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-22Remove unnecessary width field, the width is part of the APInt.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73872 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-22Store ConstantExpr's value as an APInt.Daniel Dunbar
- In anticipation of supporting large constant values. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73871 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-22Add ConstantExpr::toString (instead of using getConstantValue()).Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73870 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Start SimplifyingExprBuilderDaniel Dunbar
- Normalize Ne, Ugt, Uge, Slt, Sge git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73458 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-15Support partial folding for Add in new constant folding builder.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73363 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Add NonConstantExpr, so it is possible to statically type an expression that isDaniel Dunbar
known to be not-constant. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73352 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Rename FoldingExprBuilder -> SimplifyingExprBuilderDaniel Dunbar
Also, start printing query # with -print-ast (for testing purposes). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73350 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Kill off ExtractExpr::createByteOff.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73348 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Use ExprBuilder for constructing expressions in the Parser.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73345 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Add ExprBuilder base class, and start of implementations.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73339 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14More ConstantExpr cleanup.Daniel Dunbar
- Change Executor::evalConstant to return ConstantExpr. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73337 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Remove some unused functionality.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73329 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Add ConstantExpr::{getLimitedValue,getZExtValue}.Daniel Dunbar
- For use in situations where the range of the constant is known to fit in a uint64 (or smaller), or the extra bits don't matter. - No (intended) functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73326 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Rewrite ImpliedValue to use ConstantExpr operations.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73325 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Add several ConstantExpr utility functions and move clients over.Daniel Dunbar
- Reducing uses of getConstantValue() so we can move to arbitrary precision constants. - No (intended) functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73324 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Add constant folding operations to ConstantExpr.Daniel Dunbar
- No (intended) functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73322 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-13Reverted last change that added createIff. Since we only handleCristian Cadar
bitvectors, we can just use Eq. The parser can distinguish between boolean formulas and bitvector terms. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73309 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-13Added a helper function to construct IFF expressions.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73283 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Move Array construction out of MemoryObject into ObjectState.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73162 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Change ExecutionState::symbolics to include both the MemoryObject and theDaniel Dunbar
symbolic Array. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73161 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09More constant Array support.Daniel Dunbar
- The are parsed, printed, and solved now. - Remove some members of ArrayDecl which are only duplicates of Array members. - KLEE still doesn't create these, but you can write them by hand. The EXE style constant array optimization for STP (turning the initial writes into asserts) is now only a stones throw away, but I need to leave something fun to do tomorrow. :) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73133 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Add initial support for constant Arrays.Daniel Dunbar
- This doesn't actually start using them, it just attempts to update all clients to do the right thing in the presence of them. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73130 91177308-0d34-0410-b5e6-96231b3b80d8