From 393e4a2d3e4b477b04bd31c53e84fc4690e3544b Mon Sep 17 00:00:00 2001 From: "Hoang M. Le" Date: Thu, 27 Oct 2016 17:51:29 +0200 Subject: apply clang-format --- lib/Solver/MetaSMTSolver.cpp | 45 +++++++++++++++++++++----------------------- 1 file changed, 21 insertions(+), 24 deletions(-) diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index a34e26d0..a453de40 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -28,7 +28,7 @@ #undef Expr #undef Type #undef STP - + #include #include #include @@ -36,7 +36,6 @@ #include #include - static unsigned char *shared_memory_ptr; static int shared_memory_id = 0; // Darwin by default has a very small limit on the maximum amount of shared @@ -205,7 +204,7 @@ SolverImpl::SolverRunStatus MetaSMTSolverImpl::runAndGetCex( // assume the constraints of the query for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); + ie = query.constraints.end(); it != ie; ++it) { assumption(_meta_solver, _builder->construct(*it)); } @@ -291,30 +290,29 @@ MetaSMTSolverImpl::runAndGetCexForked( // asssert the negation of the query as we are in a child process assertion(_meta_solver, - _builder->construct(Expr::createIsZero(query.expr))); + _builder->construct(Expr::createIsZero(query.expr))); unsigned res = solve(_meta_solver); if (res) { - for (std::vector::const_iterator it = objects.begin(), - ie = objects.end(); - it != ie; ++it) { - - const Array *array = *it; - assert(array); - typename SolverContext::result_type array_exp = - _builder->getInitialArray(array); - - for (unsigned offset = 0; offset < array->size; offset++) { - - typename SolverContext::result_type elem_exp = - evaluate(_meta_solver, - metaSMT::logic::Array::select( - array_exp, bvuint(offset, array->getDomain()))); - unsigned char elem_value = - metaSMT::read_value(_meta_solver, elem_exp); - *pos++ = elem_value; - } + for (std::vector::const_iterator it = objects.begin(), + ie = objects.end(); + it != ie; ++it) { + + const Array *array = *it; + assert(array); + typename SolverContext::result_type array_exp = + _builder->getInitialArray(array); + + for (unsigned offset = 0; offset < array->size; offset++) { + + typename SolverContext::result_type elem_exp = evaluate( + _meta_solver, metaSMT::logic::Array::select( + array_exp, bvuint(offset, array->getDomain()))); + unsigned char elem_value = + metaSMT::read_value(_meta_solver, elem_exp); + *pos++ = elem_value; } + } } assert((uint64_t *)pos); *((uint64_t *)pos) = stats::queryConstructs; @@ -385,7 +383,6 @@ MetaSMTSolverImpl::getOperationStatusCode() { return _runStatusCode; } - template MetaSMTSolver::MetaSMTSolver(bool useForked, bool optimizeDivides) -- cgit 1.4.1