Merge pull request #376 from tautschnig/lint-cleanup

Code cleanup to increase cpplint-cleanliness

Author: kroening

src/goto-instrument/accelerate/accelerate.sh renamed to regression/acceleration/accelerate.sh

@@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "path_symex.h"
 
-//#define DEBUG
+// #define DEBUG
 
 #ifdef DEBUG
 #include <iostream>
@@ -133,26 +133,31 @@ bool path_symext::propagate(const exprt &src)
   else if(src.id()==ID_plus)
   {
     forall_operands(it, src)
-      if(!propagate(*it)) return false;
+      if(!propagate(*it))
+        return false;
     return true;
   }
   else if(src.id()==ID_array)
   {
     forall_operands(it, src)
-      if(!propagate(*it)) return false;
+      if(!propagate(*it))
+        return false;
     return true;
   }
   else if(src.id()==ID_vector)
   {
     forall_operands(it, src)
-      if(!propagate(*it)) return false;
+      if(!propagate(*it))
+        return false;
     return true;
   }
   else if(src.id()==ID_if)
   {
     const if_exprt &if_expr=to_if_expr(src);
-    if(!propagate(if_expr.true_case())) return false;
-    if(!propagate(if_expr.false_case())) return false;
+    if(!propagate(if_expr.true_case()) ||
+       !propagate(if_expr.false_case()))
+      return false;
+
     return true;
   }
   else if(src.id()==ID_array_of)
@@ -244,7 +249,8 @@ inline static typet c_sizeof_type_rec(const exprt &expr)
     forall_operands(it, expr)
     {
       typet t=c_sizeof_type_rec(*it);
-      if(t.is_not_nil()) return t;
+      if(t.is_not_nil())
+        return t;
     }
   }
 
@@ -298,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()));
           }
         }
       }
@@ -323,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);
@@ -336,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)
@@ -385,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)
@@ -446,7 +450,8 @@ void path_symext::assign_rec(
       state.record_step();
       path_symex_stept &step=*state.history;
 
-      if(!guard.empty()) step.guard=conjunction(guard);
+      if(!guard.empty())
+        step.guard=conjunction(guard);
       step.full_lhs=ssa_lhs;
       step.ssa_lhs=new_lhs;
       step.ssa_rhs=ssa_rhs;
@@ -579,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);
     }
@@ -601,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);
     }
@@ -618,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);
     }
@@ -670,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;
 
@@ -690,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();
@@ -741,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();
@@ -755,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'
@@ -767,6 +785,7 @@ void path_symext::function_call_rec(
     }
   }
   else
+    // NOLINTNEXTLINE(readability/throw) as message is correctly uppercase
     throw "TODO: function_call "+function.id_string();
 }
 
@@ -885,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));
@@ -905,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
@@ -1016,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;
     }
@@ -1028,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);
@@ -1042,7 +1061,7 @@ void path_symext::operator()(
 
   case THROW:
     state.record_step();
-    throw "THROW not yet implemented";
+    throw "THROW not yet implemented"; // NOLINT(readability/throw)
 
   case ASSUME:
     state.record_step();
@@ -1081,7 +1100,7 @@ void path_symext::operator()(
 
   case ATOMIC_END:
     if(!state.inside_atomic_section)
-      throw "ATOMIC_END unmatched";
+      throw "ATOMIC_END unmatched"; // NOLINT(readability/throw)
 
     state.record_step();
     state.next_pc();
@@ -1095,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.cpp

@@ -20,7 +20,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "path_symex_state.h"
 
-//#define DEBUG
+// #define DEBUG
 
 #ifdef DEBUG
 #include <iostream>
@@ -131,7 +131,8 @@ path_symex_statet::var_statet &path_symex_statet::get_var_state(
 
   var_valt &var_val=
     var_info.is_shared()?shared_vars:threads[current_thread].local_vars;
-  if(var_val.size()<=var_info.number) var_val.resize(var_info.number+1);
+  if(var_val.size()<=var_info.number)
+    var_val.resize(var_info.number+1);
   return var_val[var_info.number];
 }
 
@@ -150,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!
@@ -174,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;
@@ -633,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;
   }
@@ -771,7 +773,8 @@ bool path_symex_statet::check_assertion(
   exprt assertion=read(instruction.guard);
 
   // trivial?
-  if(assertion.is_true()) return true; // no error
+  if(assertion.is_true())
+    return true; // no error
 
   // the path constraint
   decision_procedure << history;