diff options
| author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-05-30 17:12:30 +0100 |
|---|---|---|
| committer | MartinNowack <martin.nowack@gmail.com> | 2019-06-04 11:55:50 +0200 |
| commit | 32892a0c836c6153808e2c821b86b5d36db51cbf (patch) | |
| tree | 6cd97b9b18a5e1ce874be126dcd134bf67ee5205 /lib/Solver/MetaSMTSolver.cpp | |
| parent | ade2bf89486ae2e44571fb547dbc96488fc3dab4 (diff) | |
| download | klee-32892a0c836c6153808e2c821b86b5d36db51cbf.tar.gz | |
Remove parenthesis around returns, as reported and discussed in #891
Diffstat (limited to 'lib/Solver/MetaSMTSolver.cpp')
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 26 |
1 files changed, 13 insertions, 13 deletions
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> |