about summary refs log tree commit diff homepage
path: root/lib/Solver/STPBuilder.cpp
AgeCommit message (Expand)Author
2020-05-01[Solver:STP] Fix handling of array namesMartin Nowack
2020-04-30Removed include/klee/util and moved header files to appropriate placesCristian Cadar
2020-02-19Use `ref<>` for UpdateNodeMartin Nowack
2019-09-03Moved solver-related header files into a separate klee/Solver/ directory.Cristian Cadar
2019-07-30Consolidated Expr-related include files into a single include/klee/Expr direc...Cristian Cadar
2019-06-04Remove parenthesis around returns, as reported and discussed in #891Cristian Cadar
2019-03-13Renamed --use-construct-hash to --use-construct-hash-stp and moved it and use...Cristian Cadar
2016-07-09Fix variable shifting behavior with different sizesMartin Nowack
2016-04-09Generate unique STP and Z3 array names deterministicallyMartin Nowack
2016-01-14Make it possible to build KLEE without using STP and only MetaSMT.Dan Liew
2015-12-18Move lib/Solver/SolverStats.h -> include/klee/SolverStats.hDan Liew
2015-12-04Remove dead ``tempVars`` and ``getTempVar()`` method in STPBuilderDan Liew
2015-09-22[STPBuilder] Generate SRrem expressions correctlyMartin Nowack
2015-08-30Fix signed division by constant 1/ -1Martin Nowack
2015-03-20[Solver] Fix leak intermediate expression not freedMartin Nowack
2014-12-08Fix overshift checkPaul Marinescu
2014-05-29Remove #include <iostream> to avoid static constructorsMartin Nowack
2014-04-24Fixed creation of arrays with variable domains and ranges in STPBuilder and M...Hristina Palikareva
2014-04-15Associate a domain and range with each arrayPeter Collingbourne
2014-02-14Explicitly get the width of the "shift" expression rather than assumingDan Liew
2014-02-14Fixed overshift of arithmetic right shift by constant so that itDan Liew
2014-02-14Fixed overshift of arithmetic right shift by symbolic so that it overshiftsDan Liew
2014-02-14Fixed overshift of logical right shift by constant so that itDan Liew
2014-02-14Fixed overshift of logical right shift by symbolic so that it overshiftsDan Liew
2014-02-14Fixed overshifting an expression by a constant so that we overshift toDan Liew
2014-02-14Added a test case for testing overshift behaviour of Shl and fixedDan Liew
2014-02-14Translate shl overshifts into 0Paul Marinescu
2013-08-28Fix constness warnings issued by gcc 4.7Martin Nowack
2012-10-18Nice patch by Hristina Palikareva that removes the dependency on STPCristian Cadar
2012-06-01Patch by Oscar Dustmann fixing a buffer overflow when long names areCristian Cadar
2012-03-26STPBuilder: fix bv{Zero,One,MinusOne} for the case where width>64Peter Collingbourne
2012-03-26STPBuilder: fix ConstantExpr builder for the case where width>64 butPeter Collingbourne
2011-03-30Bug fix in STPBuilder. Patch submitted by David Ramos, thanks!Cristian Cadar
2010-05-02Fix some const cast warnings.Daniel Dunbar
2009-07-10Added support for bitwise not. Replacing "false == " with Not inCristian Cadar
2009-06-26More large integer support.Daniel Dunbar
2009-06-25Flesh out support for arbitrary bit widths in some key places (STP & constantDaniel Dunbar
2009-06-14More ConstantExpr tweaks.Daniel Dunbar
2009-06-14Add ConstantExpr::{getLimitedValue,getZExtValue}.Daniel Dunbar
2009-06-14Add several ConstantExpr utility functions and move clients over.Daniel Dunbar
2009-06-09More constant Array support.Daniel Dunbar
2009-06-09Add initial support for constant Arrays.Daniel Dunbar
2009-06-09Remove Array::id.Daniel Dunbar
2009-06-05Clean up a number of unused variable warnings when building w/oDaniel Dunbar
2009-06-04Sink getConstantValue into ConstantExpr.Daniel Dunbar
2009-06-04Finish removing uses of Expr::isConstant.Daniel Dunbar
2009-06-04Start removing uses of Expr::isConstant.Daniel Dunbar
2009-06-04Use cast<> instead of static_ref_cast.Daniel Dunbar
2009-06-04Move isConstant from ref<> to Expr::Daniel Dunbar
2009-06-03Kill off specialized ref<> forwarding methods, in the interest of making it aDaniel Dunbar