From 4ddf8d3ccc054cd1be6bae25844373ed2488360a Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Sun, 30 Aug 2015 02:11:45 +0200 Subject: Allow to generate initial values with empty constraint set --- lib/Solver/IndependentSolver.cpp | 6 ++++++ test/regression/2015-08-30-empty-constraints.c | 22 ++++++++++++++++++++++ 2 files changed, 28 insertions(+) create mode 100644 test/regression/2015-08-30-empty-constraints.c 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 > &values, bool &hasSolution){ std::list * factors = new std::list; + + // 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 > 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; +} -- cgit 1.4.1