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
Age
Commit message (
Expand
)
Author
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
Add NonConstantExpr, so it is possible to statically type an expression that is
Daniel Dunbar
2009-06-14
Start test case for ConstantFoldingExprBuilder
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
Fixup syntax coloring for emacs .pc mode.
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
pcregrep should run with klee-libc.
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
Add CBE'ified version of pcregrep.
Daniel Dunbar
2009-06-13
Added a helper function to construct IFF expressions.
Cristian Cadar
2009-06-13
Removed bits of grammar dealing with quantifiers.
Cristian Cadar
2009-06-13
Support for parsing SMTLIB headers.
Cristian Cadar
2009-06-13
Changed SMTParser to return the parsed QueryCommand.
Cristian Cadar
2009-06-12
Removed parser_temp.h. Adapted the code to use SMTParser directly.
Cristian Cadar
2009-06-12
Removed unused file.
Cristian Cadar
2009-06-10
Move declaration of vc_DeleteExpr outside of function.
Daniel Dunbar
2009-06-10
Updated the SMT test driver. Other small changes to parser_temp.h and
Cristian Cadar
2009-06-10
Removed CVC3's Parser class.
Cristian Cadar
2009-06-10
Wrote a new SMTParser that inherits from klee::expr::Parser.
Cristian Cadar
2009-06-10
(Missed save) Move Array construction out of MemoryObject into ObjectState.
Daniel Dunbar
2009-06-10
Move Array construction out of MemoryObject into ObjectState.
Daniel Dunbar
2009-06-10
Change ExecutionState::symbolics to include both the MemoryObject and the
Daniel Dunbar
2009-06-10
Use Arrays instead of MemoryObject where possible.
Daniel Dunbar
2009-06-10
Fix a bug in the logging solver which was printing the expression in a
Daniel Dunbar
2009-06-10
Added a temporary driver to test the parser.
Cristian Cadar
2009-06-10
Changed expression nodes to be ExprHandle (instead of ExprHandle*), and
Cristian Cadar
2009-06-09
Use env instead of hard coding python path.
Daniel Dunbar
2009-06-09
More constant Array support.
Daniel Dunbar
2009-06-09
Do not compile SMT parser by default. Removed automatically generated
Cristian Cadar
2009-06-09
Made expression nodes int the SMT parser be pointers to ExprHandle.
Cristian Cadar
2009-06-09
Add initial support for constant Arrays.
Daniel Dunbar
[next]