Adjusts formatting according to code review

Author: ArenBabikian

src/goto-instrument/code_contracts.cpp

@@ -149,7 +149,7 @@ static void check_apply_invariants(
 
   // change the back edge into assume(false) or assume(guard)
   loop_end->targets.clear();
-  loop_end->type = ASSUME;
+  loop_end->type=ASSUME;
   if(loop_head->is_goto())
     loop_end->set_condition(false_exprt());
   else
@@ -265,7 +265,7 @@ bool code_contractst::apply_function_contract(
   }
 
   // Replace formal parameters
-  code_function_callt::argumentst::const_iterator a_it =
+  code_function_callt::argumentst::const_iterator a_it=
     call.arguments().begin();
   for(code_typet::parameterst::const_iterator p_it = type.parameters().begin();
       p_it != type.parameters().end() && a_it != call.arguments().end();
@@ -480,38 +480,38 @@ void code_contractst::instrument_call_statement(
 
     return;
   }
-  else // Called function has assigns clause
-  {
-    replace_symbolt replace;
-    // Replace formal parameters
-    code_function_callt::argumentst::const_iterator a_it =
-      call.arguments().begin();
-    for(code_typet::parameterst::const_iterator p_it =
-          called_type.parameters().begin();
-        p_it != called_type.parameters().end() &&
-        a_it != call.arguments().end();
-        ++p_it, ++a_it)
+    else // Called function has assigns clause
     {
-      if(!p_it->get_identifier().empty())
+      replace_symbolt replace;
+      // Replace formal parameters
+      code_function_callt::argumentst::const_iterator a_it =
+        call.arguments().begin();
+      for(code_typet::parameterst::const_iterator p_it =
+            called_type.parameters().begin();
+          p_it != called_type.parameters().end() &&
+          a_it != call.arguments().end();
+          ++p_it, ++a_it)
       {
-        symbol_exprt p(p_it->get_identifier(), p_it->type());
-        replace.insert(p, *a_it);
+        if(!p_it->get_identifier().empty())
+        {
+          symbol_exprt p(p_it->get_identifier(), p_it->type());
+          replace.insert(p, *a_it);
+        }
       }
-    }
 
-    replace(called_assigns);
-
-    // check compatibility of assigns clause with the called function
-    assigns_clauset called_assigns_clause(
-      called_assigns, *this, function_id, log);
-    exprt compatible =
-      assigns_clause.compatible_expression(called_assigns_clause);
-    goto_programt alias_assertion;
-    alias_assertion.add(goto_programt::make_assertion(
-      compatible, instruction_iterator->source_location));
-    program.insert_before_swap(instruction_iterator, alias_assertion);
-    ++instruction_iterator;
-  }
+      replace(called_assigns);
+
+      // check compatibility of assigns clause with the called function
+      assigns_clauset called_assigns_clause(
+        called_assigns, *this, function_id, log);
+      exprt compatible =
+        assigns_clause.compatible_expression(called_assigns_clause);
+      goto_programt alias_assertion;
+      alias_assertion.add(goto_programt::make_assertion(
+        compatible, instruction_iterator->source_location));
+      program.insert_before_swap(instruction_iterator, alias_assertion);
+      ++instruction_iterator;
+    }
 }
 
 bool code_contractst::check_for_looped_mallocs(const goto_programt &program)
@@ -785,7 +785,7 @@ void code_contractst::add_contract_check(
                        .symbol_expr();
     check.add(goto_programt::make_decl(r, skip->source_location));
 
-    call.lhs() = r;
+    call.lhs()=r;
     return_stmt = code_returnt(r);
 
     symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());

src/goto-instrument/code_contracts.h

@@ -167,8 +167,8 @@ class code_contractst
   void
   add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest);
 
-  // If the expression is a quantified expression, this function adds
-  // the quantified variable to the symbol table and to the expression map
+  /// If the expression is a quantified expression, this function adds
+  /// the quantified variable to the symbol table and to the expression map
   void add_quantified_variable(
     exprt expression,
     replace_symbolt &replace,