about summary refs log tree commit diff homepage
path: root/lib/Solver/MetaSMTBuilder.h
AgeCommit message (Collapse)Author
2019-07-30Consolidated Expr-related include files into a single include/klee/Expr ↵Cristian Cadar
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
2019-06-04make include guard naming consistentJulian Büning
2016-09-29remove mimic_stp option and the associated ITE chain construction for shift ↵Hoang M. Le
operators
2016-06-28add assertions to check the pre-condition of bvVar*Shift that both operands ↵Hoang M. Le
have the same bv width
2016-06-27change bitwidth of expr_shpost in MetaSMTBuilder::constructSDivByConstant to ↵Hoang M. Le
64, so that the first two arguments of the call bvVarRightShift(extend_npm, expr_shpost, 64) have the same bitwidth of 64.
2016-06-10apply clang-formatHoang M. Le
2016-06-10remove now unused getShiftBits()Hoang M. Le
2016-06-10remove bitmasking shift amount in bvVarArithRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvVarRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvVarLeftShiftHoang M. Le
2016-06-10remove bitmasking shift amount in constructAShrByConstant and make it return ↵Hoang M. Le
0 when overshifting
2016-06-10remove bitmasking shift amount in bvRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvLeftShiftHoang M. Le
2016-06-10handle special cases of sdiv 1 and -1Hoang M. Le
2016-06-10clean up metaSMT includesHoang M. Le
2016-02-23Added missing copyright headers per klee/issue #301Marko Dimjašević
2016-01-14Make it possible to build KLEE without using STP and only MetaSMT.Dan Liew
The default core solver is STP if KLEE is built with STP otherwise it is MetaSMT. Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for consistency.
2014-12-09Merge pull request #186 from paulmar/fixshiftCristian Cadar
Fix overshift check
2014-12-08Fix overshift checkPaul Marinescu
Shifting by bitwidth-1 is valid
2014-12-03Handling overshift behaviour in MetaSMTBuilderHristina Palikareva
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
According to LLVM: lightweight and simpler implementation of streams.
2014-04-24Fixed order of domain and range in array creation in MetaSMTBuilder.Hristina Palikareva
2014-04-24Fixed creation of arrays with variable domains and ranges in STPBuilder and ↵Hristina Palikareva
MetaSMTBuilder.
2013-10-11Bug fix in MetaSMTBuilderHristina Palikareva
2013-10-11MetaSMT builder, solver and command-line options.Hristina Palikareva
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-13 21:53:06 +0000