about summary refs log tree commit diff homepage
path: root/test/Expr
AgeCommit message (Collapse)Author
2014-04-02Modify the SMT-LIB printer to declare arrays in a deterministic ↵Peter Collingbourne
(alphabetical) order.
2014-01-20Remove the last remnants (I think) of DejaGNU. Goodbye!Dan Liew
Say hello to our new friend, llvm-lit :)
2014-01-20Fixed Expr/Parser/Simplify.pc test for llvm-lit. Escaped quote issue.Dan Liew
2014-01-20Fixed Expr/Parser/MultiByteReads.pc test.Dan Liew
2014-01-20Fixed Expr/Parser/ConstantFolding.pc test for llvm-lit (this probablyDan Liew
breaks DejaGNU tests). The issue is that in Tcl the quote needs escaping but for llvm-lit we don't need to do this. We should move to using the LLVM FileCheck tool instead of grep!
2012-10-24Patch by Dan Liew: "Added primitive test that checks kleaver's newCristian Cadar
-print-smt option. Improved Feature/ExprLogging.c test: - Now (primitive) checks the result of -write-smt2s - Now (primitive) checks the result of -write-pcs - Now (primitive) checks the result of -write-cvcs" git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166569 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-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-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-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-06-16Add basic constant folding / simplification for Eq.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73467 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Add (very) basic constant folding for And,Or,Xor.Daniel Dunbar
- Lots more important goodness can be done here. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73461 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Add (very) basic constant folding for Mul.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73460 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 Sub in new constant folding builder.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73377 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-14Start test case for ConstantFoldingExprBuilderDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73351 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-07Implement array declarations.Daniel Dunbar
- Printing current prints all declarations, and we allow redefinition, since the printer doesn't know what has already been printed. - Names don't print right yet, since the Array* object doesn't have the name. - Various things are unsupported. o Array domain/range must be w32/w8. o Concrete initializers for arrays are unsupported. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73026 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-07Update test case.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73020 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-07Eliminate anonymous versions.Daniel Dunbar
- For now, this means the isRooted flag for arrays isn't propogated to the kquery language. We should figure out how to do this, but allow anonymous versions isn't the right way. Also, improved the error on invalid writes a bit. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73018 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Support the extended query command syntax.Daniel Dunbar
- There are two optional lists following the constraints and the query expression. The first is a list of expressions to give values for and the second is a list of arrays to provide values for. - Update ExprPPrinter to accept extra arguments to print these arguments. - Add Parser support. - Add more ArrayDecl support. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72938 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Turn an assert into a parse failure.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72935 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Add evaluation support to kleaver (now the default).Daniel Dunbar
- Currently only handles validity queries. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72933 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Moved MultiByteReads.pc in test/Expr/ParserCristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72851 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Fixed a bug in Kleaver's parser: APInt does not allow "truncation" toCristian Cadar
the same width. Added a test case that was previously triggering an assert violation. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72850 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Added a couple of tests for ReadLSB/MSB. Changed kleaver to write to stdout.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72841 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Missed a couple testsDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72206 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 2024-11-30 03:30:37 +0000