index
:
~cnx/klee
this commit
1.0.x
1.1.x
1.2.x
1.3.x
1.4.x
2.0.x
2.1.x
2.2.x
2.3.x
3.0.x
master
psychic
svcomp
svcomp_32bit
KLEE fork for patch differentiation testing
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
lib
Age
Commit message (
Expand
)
Author
2009-07-10
Added support for bitwise not. Replacing "false == " with Not in
Cristian Cadar
2009-07-10
Replaced createNot() by createIsZero() and "Not" macro by "Nz".
Cristian Cadar
2009-07-08
Added support for bitvector variables to the SMTLIB parser (currently
Cristian Cadar
2009-07-02
Added support for bitvector constants to the SMTLIB parser. Only
Cristian Cadar
2009-06-27
Start move to using APFloat (support long double).
Daniel Dunbar
2009-06-26
Simplify read/write code.
Daniel Dunbar
2009-06-26
More large integer support.
Daniel Dunbar
2009-06-25
Recognizing more SMTLIB expressions (bitwise, etc.). Some of them
Cristian Cadar
2009-06-25
Added support for flets.
Cristian Cadar
2009-06-25
Simplified grammar by properly factoring out the rule for optional annotations.
Cristian Cadar
2009-06-25
Kill off last getConstantValue uses.
Daniel Dunbar
2009-06-25
Remove some more uses of getConstantValue.
Daniel Dunbar
2009-06-25
Switch to using APInt math operations.
Daniel Dunbar
2009-06-25
Flesh out support for arbitrary bit widths in some key places (STP & constant
Daniel Dunbar
2009-06-24
Update for LLVM API change.
Daniel Dunbar
2009-06-24
Added support for LET expressions. Added simple environment support
Cristian Cadar
2009-06-22
Remove unnecessary width field, the width is part of the APInt.
Daniel Dunbar
2009-06-22
Store ConstantExpr's value as an APInt.
Daniel Dunbar
2009-06-22
Add ConstantExpr::toString (instead of using getConstantValue()).
Daniel Dunbar
2009-06-22
Update for changes in how JIT is linked in.
Daniel Dunbar
2009-06-16
Improve FastCexSolver:
Daniel Dunbar
2009-06-16
Add basic constant folding / simplification for Eq.
Daniel Dunbar
2009-06-16
Add (very) basic constant folding for And,Or,Xor.
Daniel Dunbar
2009-06-16
Add (very) basic constant folding for Mul.
Daniel Dunbar
2009-06-16
Added support for comparison and arithmetic expressions.
Cristian Cadar
2009-06-16
Start SimplifyingExprBuilder
Daniel Dunbar
2009-06-16
Added bitvector function/predicate names to the lexer.
Cristian Cadar
2009-06-16
Added support for logical formulas in the SMTLIB parser.
Cristian Cadar
2009-06-15
Support partial folding for Sub in new constant folding builder.
Daniel Dunbar
2009-06-15
Support partial folding for Add in new constant folding builder.
Daniel Dunbar
2009-06-14
Rename FoldingExprBuilder -> SimplifyingExprBuilder
Daniel Dunbar
2009-06-14
Kill off ExtractExpr::createByteOff.
Daniel Dunbar
2009-06-14
The expansion for Read{MSB,LSB} needs to continue to use the folding methods,
Daniel Dunbar
2009-06-14
Use ExprBuilder for constructing expressions in the Parser.
Daniel Dunbar
2009-06-14
Remove the (A < constant) => (A == 0 || A == 1 ... || A == constant - 1)
Daniel Dunbar
2009-06-14
Add ExprBuilder base class, and start of implementations.
Daniel Dunbar
2009-06-14
More ConstantExpr cleanup.
Daniel Dunbar
2009-06-14
Fail with an exec error on large (> 64-bit) floating point ops.
Daniel Dunbar
2009-06-14
Remove some unused functionality.
Daniel Dunbar
2009-06-14
More ConstantExpr tweaks.
Daniel Dunbar
2009-06-14
Change AddressSpace::resolveOne to take a ConstantExpr directly (and to allow
Daniel Dunbar
2009-06-14
Add ConstantExpr::{getLimitedValue,getZExtValue}.
Daniel Dunbar
2009-06-14
Rewrite ImpliedValue to use ConstantExpr operations.
Daniel Dunbar
2009-06-14
Add several ConstantExpr utility functions and move clients over.
Daniel Dunbar
2009-06-14
Add constant folding operations to ConstantExpr.
Daniel Dunbar
2009-06-13
Switch to using constant arrays for non-symbolic objects.
Daniel Dunbar
2009-06-13
Reverted last change that added createIff. Since we only handle
Cristian Cadar
2009-06-13
Create new ObjectState constructor for explicitly creating symbolic objects.
Daniel Dunbar
2009-06-13
Fix for the issue reported and diagnosed by Seungbeom, where KLEE was
Cristian Cadar
2009-06-13
Added a helper function to construct IFF expressions.
Cristian Cadar
[prev]
[next]