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
/
Solver
/
FastCexSolver.cpp
Age
Commit message (
Expand
)
Author
2023-04-21
use unique_ptr all throughout the solver chain
Daniel Schemmel
2023-04-01
remove include/klee/Support/IntEvaluation.h
Daniel Schemmel
2022-06-15
Spelling Fixes
m-davis
2020-07-01
Separate constraint set and constraint manager
Martin Nowack
2020-04-30
Removed the Internal directory from include/klee
Cristian Cadar
2020-02-19
Use `ref<>` for UpdateNode
Martin Nowack
2019-09-03
Moved solver-related header files into a separate klee/Solver/ directory.
Cristian Cadar
2019-07-30
Consolidated Expr-related include files into a single include/klee/Expr direc...
Cristian Cadar
2019-07-23
Refactor ValueRange to more modern coding standards
Daniel Schemmel
2014-09-13
Add KLEE specific DEBUG macros.
Daniel Dunbar
2014-05-29
Use LLVM DEBUG macro instead of #if 0 or #if DEBUG
Martin Nowack
2014-05-29
Remove #include <iostream> to avoid static constructors
Martin Nowack
2014-05-29
Refactoring from std::ostream to llvm::raw_ostream
Martin Nowack
2014-04-16
Removing a few more hard-coded values for domains and ranges of Array objects
Hristina Palikareva
2009-09-01
Update for LLVM ostream changes.
Daniel Dunbar
2009-07-28
Move Machine constants into Context object, initialized based on the target
Daniel Dunbar
2009-07-10
Simple propagation rules for boolean not in the fast cex solver.
Cristian Cadar
2009-06-25
Remove some more uses of getConstantValue.
Daniel Dunbar
2009-06-16
Improve FastCexSolver:
Daniel Dunbar
2009-06-14
More ConstantExpr tweaks.
Daniel Dunbar
2009-06-14
Add ConstantExpr::{getLimitedValue,getZExtValue}.
Daniel Dunbar
2009-06-09
Add initial support for constant Arrays.
Daniel Dunbar
2009-06-09
Use Array* to map objects instead of id.
Daniel Dunbar
2009-06-09
Kill off UpdateList::isRooted flag.
Daniel Dunbar
2009-06-08
FastCexSolver: Start implementing exact value propogation.
Daniel Dunbar
2009-06-08
FastCexSolver: Stub out infrastructure for propogating exact values & proving
Daniel Dunbar
2009-06-08
FastCexSolver: Add exact value contents to CexObjectData.
Daniel Dunbar
2009-06-08
FastCexSolver: Rename forceExprTo* to propogatePossible*
Daniel Dunbar
2009-06-08
FastCexSolver: Lazily initialize object values and kill off ObjectFinder class.
Daniel Dunbar
2009-06-08
Kill off Concat::is[248]ByteConcat, and fix FastCexSolver for this case.
Daniel Dunbar
2009-06-08
Cleanup FastCexSolver:
Daniel Dunbar
2009-06-04
Sink getConstantValue into ConstantExpr.
Daniel Dunbar
2009-06-04
Finish removing uses of Expr::isConstant.
Daniel Dunbar
2009-06-04
Start removing uses of Expr::isConstant.
Daniel Dunbar
2009-06-04
Use cast<> instead of static_ref_cast.
Daniel Dunbar
2009-06-04
Move isConstant from ref<> to Expr::
Daniel Dunbar
2009-06-03
Kill off specialized ref<> forwarding methods, in the interest of making it a
Daniel Dunbar
2009-06-02
Use ConstantExpr::alloc instead of ref<Expr> directly
Daniel Dunbar
2009-05-21
Initial KLEE checkin.
Daniel Dunbar