about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2009-07-26Make sure final KLEE output gets on a new line.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77155 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-26TweakDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77154 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-26Ok, I caved. klee-gcc is useful, at least for now.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77136 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-17Make sure to initialize the native target, so we can make a JIT.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@76178 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-17Update for LLVM's wishy washy developers.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@76151 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-15Fixed two test cases. Cristian Cadar
The failing test case is actually (query [false] false), which should return VALID, but currently returns INVALID. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75747 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-14Update for LLVM API changes.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75626 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-11Update documentation for Not, and normalize some formatting.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75373 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
2009-07-10Fixed order of offsets in Extract.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75311 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Added xfail test: (query [false] true) should return INVALID.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75310 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Added support for not, zero_extend, and sign_extend to the SMTLIB parser.Cristian Cadar
Added support for n-ary and, or and xor. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75299 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Updated the Not operation for constants. Added extra test case for this.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75282 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Simple propagation rules for boolean not in the fast cex solver.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75242 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Small test for non-boolean Not.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75241 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-07-08Added support for bitvector variables to the SMTLIB parser (currentlyCristian Cadar
widths have to be multiples of 8). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74990 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-02Added support for bitvector constants to the SMTLIB parser. OnlyCristian Cadar
variable and array support left. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74690 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-27emacs .pc mode: Numbers should be recognized before identifiersDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74365 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-26Simplify read/write code.Daniel Dunbar
- Get rid of unnecessary special cases. - Support read/write of large integers. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74286 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-25Recognizing more SMTLIB expressions (bitwise, etc.). Some of themCristian Cadar
still need to actually be constructed. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74169 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Added support for flets.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74167 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Simplified grammar by properly factoring out the rule for optional annotations.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74165 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-25Didn't mean to check this in.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74144 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Flesh out support for arbitrary bit widths in some key places (STP & constantDaniel Dunbar
creation). - Not used yet. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74142 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-24Update for LLVM API change.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74075 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-24Added support for LET expressions. Added simple environment supportCristian Cadar
to SMTParser. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74055 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-22Update for changes in how JIT is linked in.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73868 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-20KQuery documentation: division and shift operations.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73814 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Improve FastCexSolver: Daniel Dunbar
- Bug fix, unbreak Concat propogation (recent regression). - Also, add some simple propogation for Add. - These two knock off another 50% of the queries hitting STP from the first 30s of 'dd'. - Also, add some debugging code. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73488 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-01-11 15:28:15 +0000