diff options
| -rw-r--r-- | include/klee/SolverImpl.h | 2 | ||||
| -rw-r--r-- | include/klee/util/ArrayExprHash.h | 4 | ||||
| -rw-r--r-- | lib/Solver/ConstantDivision.cpp | 4 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 26 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 6 |
5 files changed, 21 insertions, 21 deletions
diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h index 6ea06e2a..e1b1f3d2 100644 --- a/include/klee/SolverImpl.h +++ b/include/klee/SolverImpl.h @@ -103,7 +103,7 @@ namespace klee { virtual char *getConstraintLog(const Query& query) { // dummy - return(NULL); + return nullptr; } virtual void setCoreSolverTimeout(time::Span timeout) {}; diff --git a/include/klee/util/ArrayExprHash.h b/include/klee/util/ArrayExprHash.h index 32a6fc1a..e353881f 100644 --- a/include/klee/util/ArrayExprHash.h +++ b/include/klee/util/ArrayExprHash.h @@ -88,7 +88,7 @@ bool ArrayExprHash<T>::lookupArrayExpr(const Array* array, T& exp) const { exp = it->second; res = true; } - return(res); + return res; } template<class T> @@ -117,7 +117,7 @@ bool ArrayExprHash<T>::lookupUpdateNodeExpr(const UpdateNode* un, T& exp) const exp = it->second; res = true; } - return(res); + return res; } template<class T> diff --git a/lib/Solver/ConstantDivision.cpp b/lib/Solver/ConstantDivision.cpp index e62e1354..8ebf39ad 100644 --- a/lib/Solver/ConstantDivision.cpp +++ b/lib/Solver/ConstantDivision.cpp @@ -47,7 +47,7 @@ static uint32_t ones(uint32_t x) { x += (x >> 8); x += (x >> 16); - return( x & 0x0000003f ); + return x & 0x0000003f; } /* ldz(x) -- counts the number of leading zeroes in a 32-bit word */ @@ -65,7 +65,7 @@ static uint32_t ldz(uint32_t x) { static uint32_t exp_base_2(int32_t n) { uint32_t x = ~n & (n - 32); x = x >> 31; - return( x << n ); + return x << n; } // A simple algorithm: Iterate over all contiguous regions of 1 bits diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index b58319c2..dfa78e42 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -110,7 +110,7 @@ public: SolverRunStatus getOperationStatusCode(); - SolverContext &get_meta_solver() { return (_meta_solver); }; + SolverContext &get_meta_solver() { return _meta_solver; }; }; template <typename SolverContext> @@ -140,7 +140,7 @@ char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query &) { const char *msg = "Not supported"; char *buf = new char[strlen(msg) + 1]; strcpy(buf, msg); - return (buf); + return buf; } template <typename SolverContext> @@ -158,7 +158,7 @@ bool MetaSMTSolverImpl<SolverContext>::computeTruth(const Query &query, success = true; } - return (success); + return success; } template <typename SolverContext> @@ -180,7 +180,7 @@ bool MetaSMTSolverImpl<SolverContext>::computeValue(const Query &query, success = true; } - return (success); + return success; } template <typename SolverContext> @@ -215,7 +215,7 @@ bool MetaSMTSolverImpl<SolverContext>::computeInitialValues( } } - return (success); + return success; } template <typename SolverContext> @@ -260,9 +260,9 @@ SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex( } if (true == hasSolution) { - return (SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE); + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; } else { - return (SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE); + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; } } @@ -291,7 +291,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( int pid = fork(); if (pid == -1) { klee_warning("fork failed (for metaSMT)"); - return (SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED); + return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED; } if (pid == 0) { @@ -349,7 +349,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( if (res < 0) { klee_warning("waitpid() for metaSMT failed"); - return (SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED); + return SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED; } // From timed_run.py: It appears that linux at least will on @@ -359,7 +359,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( klee_warning( "error: metaSMT did not return successfully (status = %d) \n", WTERMSIG(status)); - return (SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED); + return SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED; } int exitcode = WEXITSTATUS(status); @@ -369,10 +369,10 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( hasSolution = false; } else if (exitcode == 52) { klee_warning("metaSMT timed out"); - return (SolverImpl::SOLVER_RUN_STATUS_TIMEOUT); + return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; } else { klee_warning("metaSMT did not return a recognized code"); - return (SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE); + return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE; } if (hasSolution) { @@ -415,7 +415,7 @@ MetaSMTSolver<SolverContext>::~MetaSMTSolver() {} template <typename SolverContext> char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query &query) { - return (impl->getConstraintLog(query)); + return impl->getConstraintLog(query); } template <typename SolverContext> diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 57dea28b..0bd5084a 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -462,7 +462,7 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width _arr_hash.hashArrayExpr(root, array_expr); } - return(array_expr); + return array_expr; } ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) { @@ -472,7 +472,7 @@ ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) { ::VCExpr STPBuilder::getArrayForUpdate(const Array *root, const UpdateNode *un) { if (!un) { - return(getInitialArray(root)); + return getInitialArray(root); } else { // FIXME: This really needs to be non-recursive. @@ -488,7 +488,7 @@ ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) { _arr_hash.hashUpdateNodeExpr(un, un_expr); } - return(un_expr); + return un_expr; } } |