Merge pull request #4326 from karkhaz/kk-non-functional

Pre-contracts whitespace changes

Author: tautschnig

src/analyses/dependence_graph.cpp

@@ -176,7 +176,9 @@ void dep_graph_domaint::data_dependencies(
     {
       bool found=false;
       for(const auto &wr : w_range.second)
+      {
         for(const auto &r_range : r_ranges)
+        {
           if(!found &&
              may_be_def_use_pair(wr.first, wr.second,
                                  r_range.first, r_range.second))
@@ -185,6 +187,8 @@ void dep_graph_domaint::data_dependencies(
             data_deps.insert(w_range.first);
             found=true;
           }
+        }
+      }
     }
 
     dep_graph.reaching_definitions()[to].clear_cache(it->first);

src/analyses/goto_rw.cpp

@@ -431,12 +431,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;
     }
@@ -728,7 +728,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

@@ -1334,7 +1334,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

@@ -2403,8 +2403,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

@@ -1688,11 +1688,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

@@ -466,15 +466,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();