diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Solver/ConstantDivision.cpp | 4 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 26 | ||||
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 6 |
3 files changed, 18 insertions, 18 deletions
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; } } |