diff options
author | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2014-04-16 17:56:13 +0100 |
---|---|---|
committer | Hristina Palikareva <h.palikareva@imperial.ac.uk> | 2014-04-16 18:11:55 +0100 |
commit | aa8cc67c0d8c16388ebe670757327a81f774d0ee (patch) | |
tree | 1ee1a08cff55c96cbc169a88a9516c0b933295ad /lib/Solver/Solver.cpp | |
parent | 7f44b9346356c91f633c6de6939c33a45756ae7e (diff) | |
download | klee-aa8cc67c0d8c16388ebe670757327a81f774d0ee.tar.gz |
Removing a few more hard-coded values for domains and ranges of Array objects
Diffstat (limited to 'lib/Solver/Solver.cpp')
-rw-r--r-- | lib/Solver/Solver.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 22b1545f..c61b6b1c 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -407,11 +407,12 @@ ValidatingSolver::computeInitialValues(const Query& query, std::vector< ref<Expr> > bindings; for (unsigned i = 0; i != values.size(); ++i) { const Array *array = objects[i]; + assert(array); for (unsigned j=0; j<array->size; j++) { unsigned char value = values[i][j]; bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, 0), - ConstantExpr::alloc(j, Expr::Int32)), - ConstantExpr::alloc(value, Expr::Int8))); + ConstantExpr::alloc(j, array->getDomain())), + ConstantExpr::alloc(value, array->getRange()))); } } ConstraintManager tmp(bindings); |