Whitespace and line breaks to match coding guidelines (part 2)

Author: tautschnig

src/aa-path-symex/path_symex.cpp

@@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "path_symex.h"
 
-//#define DEBUG
+// #define DEBUG
 
 #ifdef DEBUG
 #include <iostream>
@@ -304,7 +304,8 @@ void path_symext::symex_malloc(
             mp_integer elements=alloc_size/elem_size;
 
             if(elements*elem_size==alloc_size)
-              object_type=array_typet(tmp_type, from_integer(elements, tmp_size.type()));
+              object_type=
+                array_typet(tmp_type, from_integer(elements, tmp_size.type()));
           }
         }
       }
@@ -329,8 +330,6 @@ void path_symext::symex_malloc(
       size_symbol.type=tmp_size.type();
       size_symbol.mode=ID_C;
 
-      //state.var_map(size_symbol.name, suffix, size_symbol.type);
-
       assign(state,
              size_symbol.symbol_expr(),
              size);
@@ -342,15 +341,14 @@ void path_symext::symex_malloc(
   // value
   symbolt value_symbol;
 
-  value_symbol.base_name="dynamic_object"+std::to_string(state.var_map.dynamic_count);
+  value_symbol.base_name=
+    "dynamic_object"+std::to_string(state.var_map.dynamic_count);
   value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name);
   value_symbol.is_lvalue=true;
   value_symbol.type=object_type;
   value_symbol.type.set("#dynamic", true);
   value_symbol.mode=ID_C;
 
-  //state.var_map(value_symbol.name, suffix, value_symbol.type);
-
   address_of_exprt rhs;
 
   if(object_type.id()==ID_array)
@@ -391,11 +389,11 @@ void path_symext::assign_rec(
   const exprt &ssa_lhs,
   const exprt &ssa_rhs)
 {
-  //const typet &ssa_lhs_type=state.var_map.ns.follow(ssa_lhs.type());
+  // const typet &ssa_lhs_type=state.var_map.ns.follow(ssa_lhs.type());
 
   #ifdef DEBUG
   std::cout << "assign_rec: " << ssa_lhs.pretty() << std::endl;
-  //std::cout << "ssa_lhs_type: " << ssa_lhs_type.id() << std::endl;
+  // std::cout << "ssa_lhs_type: " << ssa_lhs_type.id() << std::endl;
   #endif
 
   if(ssa_lhs.id()==ID_symbol)
@@ -586,7 +584,8 @@ void path_symext::assign_rec(
     {
       exprt new_rhs=
         ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(member_exprt(ssa_rhs, components[i].get_name(), components[i].type()),
+        simplify_expr(
+          member_exprt(ssa_rhs, components[i].get_name(), components[i].type()),
           state.var_map.ns);
       assign_rec(state, guard, operands[i], new_rhs);
     }
@@ -608,7 +607,11 @@ void path_symext::assign_rec(
     {
       exprt new_rhs=
         ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(index_exprt(ssa_rhs, from_integer(i, index_type()), array_type.subtype()),
+        simplify_expr(
+          index_exprt(
+            ssa_rhs,
+            from_integer(i, index_type()),
+            array_type.subtype()),
           state.var_map.ns);
       assign_rec(state, guard, operands[i], new_rhs);
     }
@@ -625,7 +628,11 @@ void path_symext::assign_rec(
     {
       exprt new_rhs=
         ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(index_exprt(ssa_rhs, from_integer(i, index_type()), vector_type.subtype()),
+        simplify_expr(
+          index_exprt(
+            ssa_rhs,
+            from_integer(i, index_type()),
+            vector_type.subtype()),
           state.var_map.ns);
       assign_rec(state, guard, operands[i], new_rhs);
     }
@@ -677,7 +684,9 @@ void path_symext::function_call_rec(
       state.locs.function_map.find(function_identifier);
 
     if(f_it==state.locs.function_map.end())
-      throw "failed to find `"+id2string(function_identifier)+"' in function_map";
+      throw
+        "failed to find `"+id2string(function_identifier)+
+        "' in function_map";
 
     const locst::function_entryt &function_entry=f_it->second;
 
@@ -697,7 +706,8 @@ void path_symext::function_call_rec(
     }
 
     // push a frame on the call stack
-    path_symex_statet::threadt &thread=state.threads[state.get_current_thread()];
+    path_symex_statet::threadt &thread=
+      state.threads[state.get_current_thread()];
     thread.call_stack.push_back(path_symex_statet::framet());
     thread.call_stack.back().current_function=function_identifier;
     thread.call_stack.back().return_location=thread.pc.next_loc();
@@ -748,7 +758,7 @@ void path_symext::function_call_rec(
     const if_exprt &if_expr=to_if_expr(function);
     exprt guard=if_expr.cond();
 
-    if (state.is_lazy())
+    if(state.is_lazy())
     {
       const exprt &case_expr=state.restore_branch()?
         if_expr.true_case():if_expr.false_case();
@@ -762,7 +772,8 @@ void path_symext::function_call_rec(
         path_symex_statet &false_state=further_states.back();
         false_state.record_branch_step(false);
         false_state.history->guard=not_exprt(guard);
-        function_call_rec(further_states.back(), call, if_expr.false_case(), further_states);
+        function_call_rec(
+          further_states.back(), call, if_expr.false_case(), further_states);
       }
 
       // do the true-case in 'state'
@@ -893,11 +904,10 @@ void path_symext::do_goto(
 #endif
 
 #ifdef PATH_SYMEX_FORK
-    if (pid==-1)
-      // forking failed so continue as if PATH_SYMEX_FORK were undefined
+    // forking failed so continue as if PATH_SYMEX_FORK were undefined
+    if(pid==-1) // NOLINT(readability/braces)
 #endif
     {
-
 #ifdef PATH_SYMEX_LAZY_STATE
       // lazily copy the state into 'further_states'
       further_states.push_back(path_symex_statet::lazy_copy(state));
@@ -913,9 +923,9 @@ void path_symext::do_goto(
   }
 
 #ifdef PATH_SYMEX_FORK
-  if (pid!=0)
-    // parent process (regardless of any possible fork errors)
-    // should finish to explore all current 'further_states'
+  // parent process (regardless of any possible fork errors)
+  // should finish to explore all current 'further_states'
+  if(pid!=0) // NOLINT(readability/braces)
 #endif
   {
     // branch not taken case
@@ -1024,7 +1034,8 @@ void path_symext::operator()(
 
       // ordering of the following matters due to vector instability
       path_symex_statet::threadt &new_thread=state.add_thread();
-      path_symex_statet::threadt &old_thread=state.threads[state.get_current_thread()];
+      path_symex_statet::threadt &old_thread=
+        state.threads[state.get_current_thread()];
       new_thread.pc=loc.branch_target;
       new_thread.local_vars=old_thread.local_vars;
     }
@@ -1036,7 +1047,7 @@ void path_symext::operator()(
     break;
 
   case GOTO:
-    if (state.is_lazy())
+    if(state.is_lazy())
       do_goto(state, state.restore_branch());
     else
       do_goto(state, further_states);
@@ -1103,7 +1114,8 @@ void path_symext::operator()(
 
   case FUNCTION_CALL:
     state.record_step();
-    function_call(state, to_code_function_call(instruction.code), further_states);
+    function_call(
+      state, to_code_function_call(instruction.code), further_states);
     break;
 
   case OTHER:

src/aa-path-symex/path_symex_state.cpp

@@ -20,7 +20,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "path_symex_state.h"
 
-//#define DEBUG
+// #define DEBUG
 
 #ifdef DEBUG
 #include <iostream>
@@ -151,7 +151,7 @@ Function: path_symex_statet::read
 exprt path_symex_statet::read(const exprt &src, bool propagate)
 {
   #ifdef DEBUG
-  //std::cout << "path_symex_statet::read " << src.pretty() << std::endl;
+  // std::cout << "path_symex_statet::read " << src.pretty() << std::endl;
   #endif
 
   // This has five phases!
@@ -175,7 +175,7 @@ exprt path_symex_statet::read(const exprt &src, bool propagate)
   exprt tmp5=simplify_expr(tmp4, var_map.ns);
 
   #ifdef DEBUG
-  //std::cout << " ==> " << tmp.pretty() << std::endl;
+  // std::cout << " ==> " << tmp.pretty() << std::endl;
   #endif
 
   return tmp5;
@@ -634,7 +634,8 @@ exprt path_symex_statet::instantiate_rec_address(
   {
     if_exprt if_expr=to_if_expr(src);
     if_expr.true_case()=instantiate_rec_address(if_expr.true_case(), propagate);
-    if_expr.false_case()=instantiate_rec_address(if_expr.false_case(), propagate);
+    if_expr.false_case()=
+      instantiate_rec_address(if_expr.false_case(), propagate);
     if_expr.cond()=instantiate_rec(if_expr.cond(), propagate);
     return if_expr;
   }

src/aa-symex/path_search.cpp

@@ -177,7 +177,7 @@ path_searcht::resultt path_searcht::operator()(
   {
     // either a child found and reported a bug or
     // the parent's search partition is safe
-    switch (exit_status)
+    switch(exit_status)
     {
     case 0: return SAFE;
     case 10: return UNSAFE;

src/analyses/cfg_dominators.h

@@ -149,13 +149,15 @@ void cfg_dominators_templatet<P, T, post_dom>::fixedpoint(P &program)
     bool changed=false;
     typename cfgt::nodet &node=cfg[cfg.entry_map[current]];
     if(node.dominators.empty())
+    {
       for(const auto &edge : (post_dom ? node.out : node.in))
         if(!cfg[edge.first].dominators.empty())
         {
           node.dominators=cfg[edge.first].dominators;
           node.dominators.insert(current);
           changed=true;
         }
+    }
 
     // compute intersection of predecessors
     for(const auto &edge : (post_dom ? node.out : node.in))
@@ -200,7 +202,7 @@ void cfg_dominators_templatet<P, T, post_dom>::fixedpoint(P &program)
 
     if(changed) // fixed point for node reached?
     {
-      for(const auto & edge : (post_dom?node.in:node.out))
+      for(const auto &edge : (post_dom ? node.in : node.out))
       {
         worklist.push_back(cfg[edge.first].PC);
       }
@@ -263,10 +265,12 @@ void cfg_dominators_templatet<P, T, post_dom>::output(std::ostream &out) const
   }
 }
 
-typedef cfg_dominators_templatet<const goto_programt, goto_programt::const_targett, false>
+typedef cfg_dominators_templatet<
+          const goto_programt, goto_programt::const_targett, false>
         cfg_dominatorst;
 
-typedef cfg_dominators_templatet<const goto_programt, goto_programt::const_targett, true>
+typedef cfg_dominators_templatet<
+          const goto_programt, goto_programt::const_targett, true>
         cfg_post_dominatorst;
 
 template<>

src/analyses/constant_propagator.cpp

@@ -6,7 +6,7 @@ Author: Peter Schrammel
 
 \*******************************************************************/
 
-//#define DEBUG
+// #define DEBUG
 
 #ifdef DEBUG
 #include <iostream>
@@ -52,7 +52,7 @@ void constant_propagator_domaint::assign_rec(
       values.set_to_top(to_symbol_expr(lhs));
   }
 #if 0
-  else //TODO: could make field or array element-sensitive
+  else // TODO: could make field or array element-sensitive
   {
   }
 #endif
@@ -273,7 +273,8 @@ Function: constant_propagator_domaint::valuest::is_constant_address_of
 
 \*******************************************************************/
 
-bool constant_propagator_domaint::valuest::is_constant_address_of(const exprt &expr) const
+bool constant_propagator_domaint::valuest::is_constant_address_of(
+  const exprt &expr) const
 {
   if(expr.id()==ID_index)
     return is_constant_address_of(to_index_expr(expr).array()) &&
@@ -380,11 +381,11 @@ Function: constant_propagator_domaint::valuest::merge
 
 bool constant_propagator_domaint::valuest::merge(const valuest &src)
 {
-  //nothing to do
+  // nothing to do
   if(src.is_bottom)
     return false;
 
-  //just copy
+  // just copy
   if(is_bottom)
   {
     replace_const = src.replace_const;
@@ -394,7 +395,7 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
 
   bool changed = false;
 
-  //set everything to top that is not in src
+  // set everything to top that is not in src
   for(replace_symbolt::expr_mapt::const_iterator
         it=replace_const.expr_map.begin();
       it!=replace_const.expr_map.end();
@@ -403,7 +404,7 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
     if(src.replace_const.expr_map.find(it->first) ==
        src.replace_const.expr_map.end())
     {
-      //cannot use set_to_top here
+      // cannot use set_to_top here
       replace_const.expr_map.erase(it++);
       changed = true;
     }
@@ -557,7 +558,8 @@ void constant_propagator_ait::replace(
     }
     else if(it->is_function_call())
     {
-      s_it->second.values.replace_const(to_code_function_call(it->code).function());
+      s_it->second.values.replace_const(
+        to_code_function_call(it->code).function());
       simplify_expr(to_code_function_call(it->code).function(), ns);
 
       exprt::operandst &args =

src/analyses/custom_bitvector_analysis.cpp

@@ -387,7 +387,8 @@ void custom_bitvector_domaint::transform(
 
   case FUNCTION_CALL:
     {
-      const code_function_callt &code_function_call=to_code_function_call(instruction.code);
+      const code_function_callt &code_function_call=
+        to_code_function_call(instruction.code);
       const exprt &function=code_function_call.function();
 
       if(function.id()==ID_symbol)

src/analyses/custom_bitvector_analysis.h

@@ -132,7 +132,10 @@ class custom_bitvector_analysist:public ait<custom_bitvector_domaint>
 {
 public:
   void instrument(goto_functionst &);
-  void check(const namespacet &, const goto_functionst &, bool xml, std::ostream &);
+  void check(
+    const namespacet &,
+    const goto_functionst &,
+    bool xml, std::ostream &);
 
   exprt eval(const exprt &src, locationt loc)
   {

src/analyses/dependence_graph.cpp

@@ -355,7 +355,7 @@ void dependence_grapht::add_dep(
 
   // add_edge is redundant as the subsequent operations also insert
   // entries into the edge maps (implicitly)
-  //add_edge(n_from, n_to);
+  // add_edge(n_from, n_to);
   nodes[n_from].out[n_to].add(kind);
   nodes[n_to].in[n_from].add(kind);
 }