Merge pull request #275 from MartinNowack/fix_empty_constraints_indep_solver

Allow to generate initial values for queries with empty constraint set.

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;
+}