about summary refs log tree commit diff homepage
path: root/lib/Solver/Solver.cpp
AgeCommit message (Collapse)Author
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-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
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-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-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-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-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-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-09Kill off UpdateList::isRooted flag.Daniel Dunbar
- The right way to handle this is by using constant arrays, where the semantics are easier to define and implement. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73124 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Add klee::createDummySolver, the dummy solver always fails.Daniel Dunbar
- Useful as an alternative backend to STP for testing. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73048 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Clean up a number of unused variable warnings when building w/oDaniel Dunbar
asserts. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72924 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Change Solver::getValue to make explicit that result is a ConstantExpr.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72860 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Finish removing uses of Expr::isConstant.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72859 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Start removing uses of Expr::isConstant.Daniel Dunbar
- These should use cast<>, isa<>, or dyn_cast<> as appropriate (or better yet, changed to use ref<ConstantExpr> when the type is known). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72857 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Move isConstant from ref<> to Expr::Daniel Dunbar
- Ref.h is now freestanding. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72824 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-03Kill off specialized ref<> forwarding methods, in the interest of making it aDaniel Dunbar
more standard reference counting wrapper. - The only interesting changes here are in Ref.h, everything else is just updating foo.method to use foo->method instead. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72777 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-02Use ConstantExpr::alloc instead of ref<Expr> directlyDaniel Dunbar
- The "constant optimization" embedded inside ref<Expr> is going away. - No functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72730 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-25Add includes to get sprintf (STPBuilder) andDuncan Sands
fprintf, stderr etc (Solver) when compiling with gcc-4.4. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72381 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-22Add missing include (for FreeBSD build)Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72270 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Initial KLEE checkin.Daniel Dunbar
- Lots more tweaks, documentation, and web page content is needed, but this should compile & work on OS X & Linux. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-04-28 13:14:45 +0000