about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorHoang M. Le <hle@informatik.uni-bremen.de>2016-10-27 17:51:29 +0200
committerHoang M. Le <hle@informatik.uni-bremen.de>2016-10-27 17:51:29 +0200
commit393e4a2d3e4b477b04bd31c53e84fc4690e3544b (patch)
treedebecf2d3c05ef676cf267003f7b21e608aef941
parent71214ea259ee62e3484b1ca6ff516a6c2a66fdc2 (diff)
downloadklee-393e4a2d3e4b477b04bd31c53e84fc4690e3544b.tar.gz
apply clang-format
-rw-r--r--lib/Solver/MetaSMTSolver.cpp45
1 files changed, 21 insertions, 24 deletions
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index a34e26d0..a453de40 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -28,7 +28,7 @@
 #undef Expr
 #undef Type
 #undef STP
-  
+
 #include <errno.h>
 #include <unistd.h>
 #include <signal.h>
@@ -36,7 +36,6 @@
 #include <sys/ipc.h>
 #include <sys/shm.h>
 
-
 static unsigned char *shared_memory_ptr;
 static int shared_memory_id = 0;
 // Darwin by default has a very small limit on the maximum amount of shared
@@ -205,7 +204,7 @@ SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(
 
   // assume the constraints of the query
   for (ConstraintManager::const_iterator it = query.constraints.begin(),
-                                           ie = query.constraints.end();
+                                         ie = query.constraints.end();
        it != ie; ++it) {
     assumption(_meta_solver, _builder->construct(*it));
   }
@@ -291,30 +290,29 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
 
     // asssert the negation of the query as we are in a child process
     assertion(_meta_solver,
-               _builder->construct(Expr::createIsZero(query.expr)));
+              _builder->construct(Expr::createIsZero(query.expr)));
     unsigned res = solve(_meta_solver);
 
     if (res) {
-        for (std::vector<const Array *>::const_iterator it = objects.begin(),
-                                                        ie = objects.end();
-             it != ie; ++it) {
-
-          const Array *array = *it;
-          assert(array);
-          typename SolverContext::result_type array_exp =
-              _builder->getInitialArray(array);
-
-          for (unsigned offset = 0; offset < array->size; offset++) {
-
-            typename SolverContext::result_type elem_exp =
-                evaluate(_meta_solver,
-                         metaSMT::logic::Array::select(
-                             array_exp, bvuint(offset, array->getDomain())));
-            unsigned char elem_value =
-                metaSMT::read_value(_meta_solver, elem_exp);
-            *pos++ = elem_value;
-          }
+      for (std::vector<const Array *>::const_iterator it = objects.begin(),
+                                                      ie = objects.end();
+           it != ie; ++it) {
+
+        const Array *array = *it;
+        assert(array);
+        typename SolverContext::result_type array_exp =
+            _builder->getInitialArray(array);
+
+        for (unsigned offset = 0; offset < array->size; offset++) {
+
+          typename SolverContext::result_type elem_exp = evaluate(
+              _meta_solver, metaSMT::logic::Array::select(
+                                array_exp, bvuint(offset, array->getDomain())));
+          unsigned char elem_value =
+              metaSMT::read_value(_meta_solver, elem_exp);
+          *pos++ = elem_value;
         }
+      }
     }
     assert((uint64_t *)pos);
     *((uint64_t *)pos) = stats::queryConstructs;
@@ -385,7 +383,6 @@ MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() {
   return _runStatusCode;
 }
 
-
 template <typename SolverContext>
 MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked,
                                             bool optimizeDivides)