Whitespace fixes in prep for contracts patchset

This commit is whitespace changes to code that will be changed in a
future commit. The code changes will all be fairly subtle, so this
commit aims to do the whitespace changes in advance to make reviewers'
lives easier.

Author: karkhaz

src/analyses/goto_rw.cpp

@@ -432,12 +432,18 @@ void rw_range_sett::get_objects_address_of(const exprt &object)
      object.id() == ID_label ||
      object.id() == ID_array ||
      object.id() == ID_null_object)
+  {
     // constant, nothing to do
     return;
+  }
   else if(object.id()==ID_symbol)
+  {
     get_objects_rec(get_modet::READ, object);
+  }
   else if(object.id()==ID_dereference)
+  {
     get_objects_rec(get_modet::READ, object);
+  }
   else if(object.id()==ID_index)
   {
     const index_exprt &index=to_index_expr(object);

src/solvers/flattening/bv_pointers.cpp

@@ -54,9 +54,9 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
       literalt l=prop.new_variable();
 
       postponed_list.push_back(postponedt());
-      postponed_list.back().op=convert_bv(operands[0]);
+      postponed_list.back().op = convert_bv(operands[0]);
       postponed_list.back().bv.push_back(l);
-      postponed_list.back().expr=expr;
+      postponed_list.back().expr = expr;
 
       return l;
     }
@@ -734,7 +734,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
 void bv_pointerst::do_postponed(
   const postponedt &postponed)
 {
-  if(postponed.expr.id()==ID_dynamic_object)
+  if(postponed.expr.id() == ID_dynamic_object)
   {
     const pointer_logict::objectst &objects=
       pointer_logic.objects;

src/solvers/smt2/smt2_conv.cpp

@@ -1398,7 +1398,7 @@ void smt2_convt::convert_expr(const exprt &expr)
     if(ext>0)
       out << ")"; // zero_extend
   }
-  else if(expr.id()==ID_dynamic_object)
+  else if(expr.id() == ID_dynamic_object)
   {
     convert_is_dynamic_object(expr);
   }

src/util/simplify_expr.cpp

@@ -2166,8 +2166,10 @@ bool simplify_exprt::simplify_node(exprt &expr)
     result=simplify_byte_extract(to_byte_extract_expr(expr)) && result;
   else if(expr.id()==ID_pointer_object)
     result=simplify_pointer_object(expr) && result;
-  else if(expr.id()==ID_dynamic_object)
-    result=simplify_dynamic_object(expr) && result;
+  else if(expr.id() == ID_dynamic_object)
+  {
+    result = simplify_dynamic_object(expr) && result;
+  }
   else if(expr.id()==ID_invalid_pointer)
     result=simplify_invalid_pointer(expr) && result;
   else if(expr.id()==ID_object_size)

src/util/simplify_expr_int.cpp

@@ -1706,11 +1706,12 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
       if(expr.op0().id()==ID_address_of &&
          expr.op0().operands().size()==1)
       {
-        if(expr.op0().op0().id()==ID_symbol ||
-           expr.op0().op0().id()==ID_dynamic_object ||
-           expr.op0().op0().id()==ID_member ||
-           expr.op0().op0().id()==ID_index ||
-           expr.op0().op0().id()==ID_string_constant)
+        if(
+          expr.op0().op0().id() == ID_symbol ||
+          expr.op0().op0().id() == ID_dynamic_object ||
+          expr.op0().op0().id() == ID_member ||
+          expr.op0().op0().id() == ID_index ||
+          expr.op0().op0().id() == ID_string_constant)
         {
           expr=false_exprt();
           return false;

src/util/simplify_expr_pointer.cpp

@@ -463,15 +463,18 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
 
     if(op.id()==ID_address_of)
     {
-      if(op.operands().size()!=1 ||
-         (op.op0().id()!=ID_symbol &&
-          op.op0().id()!=ID_dynamic_object &&
-          op.op0().id()!=ID_string_constant))
+      if(
+        op.operands().size() != 1 ||
+        (op.op0().id() != ID_symbol && op.op0().id() != ID_dynamic_object &&
+         op.op0().id() != ID_string_constant))
+      {
         return true;
+      }
     }
-    else if(op.id()!=ID_constant ||
-            op.get(ID_value)!=ID_NULL)
+    else if(op.id() != ID_constant || op.get(ID_value) != ID_NULL)
+    {
       return true;
+    }
   }
 
   bool equal=expr.op0().op0()==expr.op1().op0();