Clang-format

Author: peterschrammel

src/goto-checker/symex_bmc.cpp

@@ -15,8 +15,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <limits>
 
-#include <util/source_location.h>
 #include <util/simplify_expr.h>
+#include <util/source_location.h>
 
 symex_bmct::symex_bmct(
   message_handlert &mh,
@@ -35,28 +35,28 @@ void symex_bmct::symex_step(
   const get_goto_functiont &get_goto_function,
   statet &state)
 {
-  const source_locationt &source_location=state.source.pc->source_location;
+  const source_locationt &source_location = state.source.pc->source_location;
 
-  if(!source_location.is_nil() && last_source_location!=source_location)
+  if(!source_location.is_nil() && last_source_location != source_location)
   {
-    log.debug() << "BMC at " << source_location.as_string()
-                << " (depth " << state.depth << ')' << log.eom;
+    log.debug() << "BMC at " << source_location.as_string() << " (depth "
+                << state.depth << ')' << log.eom;
 
-    last_source_location=source_location;
+    last_source_location = source_location;
   }
 
-  const goto_programt::const_targett cur_pc=state.source.pc;
-  const guardt cur_guard=state.guard;
+  const goto_programt::const_targett cur_pc = state.source.pc;
+  const guardt cur_guard = state.guard;
 
-  if(!state.guard.is_false() &&
-     state.source.pc->is_assume() &&
-     simplify_expr(state.source.pc->guard, ns).is_false())
+  if(
+    !state.guard.is_false() && state.source.pc->is_assume() &&
+    simplify_expr(state.source.pc->guard, ns).is_false())
   {
     log.statistics() << "aborting path on assume(false) at "
                      << state.source.pc->source_location << " thread "
                      << state.source.thread_nr;
 
-    const irep_idt &c=state.source.pc->source_location.get_comment();
+    const irep_idt &c = state.source.pc->source_location.get_comment();
     if(!c.empty())
       log.statistics() << ": " << c;
 
@@ -77,9 +77,9 @@ void symex_bmct::symex_step(
     // taken an impossible transition); thus we synthesize a
     // transition from the goto instruction to its target to make
     // sure the goto is considered covered
-    if(cur_pc->is_goto() &&
-       cur_pc->get_target()!=state.source.pc &&
-       cur_pc->guard.is_true())
+    if(
+      cur_pc->is_goto() && cur_pc->get_target() != state.source.pc &&
+      cur_pc->guard.is_true())
       symex_coverage.covered(cur_pc, cur_pc->get_target());
     else if(!state.guard.is_false())
       symex_coverage.covered(cur_pc, state.source.pc);
@@ -90,18 +90,18 @@ void symex_bmct::merge_goto(
   const statet::goto_statet &goto_state,
   statet &state)
 {
-  const goto_programt::const_targett prev_pc=goto_state.source.pc;
-  const guardt prev_guard=goto_state.guard;
+  const goto_programt::const_targett prev_pc = goto_state.source.pc;
+  const guardt prev_guard = goto_state.guard;
 
   goto_symext::merge_goto(goto_state, state);
 
   PRECONDITION(prev_pc->is_goto());
-  if(record_coverage &&
-     // could the branch possibly be taken?
-     !prev_guard.is_false() &&
-     !state.guard.is_false() &&
-     // branches only, no single-successor goto
-     !prev_pc->guard.is_true())
+  if(
+    record_coverage &&
+    // could the branch possibly be taken?
+    !prev_guard.is_false() && !state.guard.is_false() &&
+    // branches only, no single-successor goto
+    !prev_pc->guard.is_true())
     symex_coverage.covered(prev_pc, state.source.pc);
 }
 
@@ -110,10 +110,10 @@ bool symex_bmct::should_stop_unwind(
   const goto_symex_statet::call_stackt &context,
   unsigned unwind)
 {
-  const irep_idt id=goto_programt::loop_id(*source.pc);
+  const irep_idt id = goto_programt::loop_id(*source.pc);
 
   tvt abort_unwind_decision;
-  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
+  unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
 
   for(auto handler : loop_unwind_handlers)
   {
@@ -127,7 +127,7 @@ bool symex_bmct::should_stop_unwind(
   // / --unwind options to decide:
   if(abort_unwind_decision.is_unknown())
   {
-    auto limit=unwindset.get_limit(id, source.thread_nr);
+    auto limit = unwindset.get_limit(id, source.thread_nr);
 
     if(!limit.has_value())
       abort_unwind_decision = tvt(false);
@@ -142,7 +142,7 @@ bool symex_bmct::should_stop_unwind(
   log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
                    << " iteration " << unwind;
 
-  if(this_loop_limit!=std::numeric_limits<unsigned>::max())
+  if(this_loop_limit != std::numeric_limits<unsigned>::max())
     log.statistics() << " (" << this_loop_limit << " max)";
 
   log.statistics() << " " << source.pc->source_location << " thread "
@@ -157,7 +157,7 @@ bool symex_bmct::get_unwind_recursion(
   unsigned unwind)
 {
   tvt abort_unwind_decision;
-  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
+  unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
 
   for(auto handler : recursion_unwind_handlers)
   {
@@ -170,7 +170,7 @@ bool symex_bmct::get_unwind_recursion(
   // / --unwind options to decide:
   if(abort_unwind_decision.is_unknown())
   {
-    auto limit=unwindset.get_limit(id, thread_nr);
+    auto limit = unwindset.get_limit(id, thread_nr);
 
     if(!limit.has_value())
       abort_unwind_decision = tvt(false);
@@ -182,14 +182,14 @@ bool symex_bmct::get_unwind_recursion(
     abort_unwind_decision.is_known(), "unwind decision should be taken by now");
   bool abort = abort_unwind_decision.is_true();
 
-  if(unwind>0 || abort)
+  if(unwind > 0 || abort)
   {
-    const symbolt &symbol=ns.lookup(id);
+    const symbolt &symbol = ns.lookup(id);
 
     log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion "
                      << symbol.display_name() << " iteration " << unwind;
 
-    if(this_loop_limit!=std::numeric_limits<unsigned>::max())
+    if(this_loop_limit != std::numeric_limits<unsigned>::max())
       log.statistics() << " (" << this_loop_limit << " max)";
 
     log.statistics() << log.eom;

src/goto-checker/symex_bmc.h

@@ -15,14 +15,14 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 #include <util/threeval.h>
 
-#include <goto-symex/path_storage.h>
 #include <goto-symex/goto_symex.h>
+#include <goto-symex/path_storage.h>
 
 #include <goto-instrument/unwindset.h>
 
 #include "symex_coverage.h"
 
-class symex_bmct: public goto_symext
+class symex_bmct : public goto_symext
 {
 public:
   symex_bmct(
@@ -41,9 +41,8 @@ class symex_bmct: public goto_symext
   /// information for the user (e.g. "unwinding iteration N, max M"), and is not
   /// enforced. They return true to halt unwinding, false to authorise
   /// unwinding, or Unknown to indicate they have no opinion.
-  typedef
-    std::function<tvt(
-      const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)>
+  typedef std::function<
+    tvt(const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)>
     loop_unwind_handlert;
 
   /// Recursion unwind handlers take the function ID, the unwind count so far,