about summary refs log tree commit diff homepage
path: root/include
AgeCommit message (Collapse)Author
2011-07-29Sign extend, rather than zero extend, narrow gep indicesPeter Collingbourne
For example, clang creates these for ++ and -- operations on pointers on 64-bit platforms. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136474 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-20Updates for LLVM 3.0. Based on changes by arrowdodger, thanks!Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135598 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-20Deprecate LLVM_VERSION_MAJOR and LLVM_VERSION_MINOR in favour ofPeter Collingbourne
version codes. This makes the preprocessor-based version tests more concise and less error prone. Also, fix the version tests in lib/Expr/Parser.cpp (immutable zext and trunc were introduced in LLVM 2.9); now 2.9 passes "make test". git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135583 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-25Name symbolic arrays using the 3rd argument to klee_make_symbolic,Peter Collingbourne
and make sure the name is unique. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@132054 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Maintain an equivalence set during comparison operationsPeter Collingbourne
This results in a significant speedup of certain comparisons involving large partially shared expression trees. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131585 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-23Fixed bug reported by Li Xuan Ji and Ayrat Khalimov.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@130070 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-23Patch by arrowdodger ↵Cristian Cadar
(http://keeda.stanford.edu/pipermail/klee-dev/2011-April/000617.html) for compiling KLEE with the latest LLVM changes. Tested against LLVM 2.7 and 2.8. The AsmAddresses test fails in 2.8 unless assertions are explicitely enabled (--enable-assertions). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@130065 91177308-0d34-0410-b5e6-96231b3b80d8
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