diff options
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 6 | ||||
| -rw-r--r-- | test/regression/2015-08-30-empty-constraints.c | 22 |
2 files changed, 28 insertions, 0 deletions
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index cfe1bb16..a7685e46 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -454,6 +454,12 @@ bool IndependentSolver::computeInitialValues(const Query& query, std::vector< std::vector<unsigned char> > &values, bool &hasSolution){ std::list<IndependentElementSet> * factors = new std::list<IndependentElementSet>; + + // We assume the query has a solution except proven differently + // This is important in case we don't have any constraints but + // we need initial values for requested array objects. + hasSolution = true; + getAllIndependentConstraintsSets(query, factors); //Used to rearrange all of the answers into the correct order std::map<const Array*, std::vector<unsigned char> > retMap; diff --git a/test/regression/2015-08-30-empty-constraints.c b/test/regression/2015-08-30-empty-constraints.c new file mode 100644 index 00000000..81439e21 --- /dev/null +++ b/test/regression/2015-08-30-empty-constraints.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t.bc 2> %t.log +// RUN: FileCheck -input-file=%t.log %s + +/** + * This test generates one execution state without constraints. + * + * The state gets terminated (in this case return) and initial values + * are generated. + * Make sure we are able to generate an input. + */ +int main() { + int d; + + klee_make_symbolic( &d, sizeof(d) ); + + // CHECK-NOT: unable to compute initial values (invalid constraints?)! + if ((d & 2) / 4) + return 1; + return 0; +} |