about summary refs log tree commit diff homepage
path: root/lib/Solver
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/Solver
parentade2bf89486ae2e44571fb547dbc96488fc3dab4 (diff)
downloadklee-32892a0c836c6153808e2c821b86b5d36db51cbf.tar.gz
Remove parenthesis around returns, as reported and discussed in #891
Diffstat (limited to 'lib/Solver')
-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;
   }
 }