aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-05-30 17:12:30 +0100
committerMartinNowack <martin.nowack@gmail.com>2019-06-04 11:55:50 +0200
commit32892a0c836c6153808e2c821b86b5d36db51cbf (patch)
tree6cd97b9b18a5e1ce874be126dcd134bf67ee5205 /lib
parentade2bf89486ae2e44571fb547dbc96488fc3dab4 (diff)
downloadklee-32892a0c836c6153808e2c821b86b5d36db51cbf.tar.gz
Remove parenthesis around returns, as reported and discussed in #891
Diffstat (limited to 'lib')
-rw-r--r--lib/Solver/ConstantDivision.cpp4
-rw-r--r--lib/Solver/MetaSMTSolver.cpp26
-rw-r--r--lib/Solver/STPBuilder.cpp6
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;
}
}