Apply formating

Author: NlightNFotis

src/goto-symex/build_goto_trace.cpp

@@ -91,9 +91,9 @@ exprt build_full_lhs_rec(
   else if(id==ID_byte_extract_little_endian ||
           id==ID_byte_extract_big_endian)
   {
-  	DATA_INVARIANT(
-    	src_original.operands().size() == 2,
-    	"byte extract expressions require two operands");
+    DATA_INVARIANT(
+      src_original.operands().size() == 2,
+      "byte extract expressions require two operands");
     exprt tmp=src_original;
     tmp.op0()=build_full_lhs_rec(prop_conv, ns, tmp.op0(), src_ssa.op0());
 

src/goto-symex/goto_symex_state.cpp

@@ -187,8 +187,7 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
   else if(expr.id()==ID_member)
   {
     DATA_INVARIANT(
-    	expr.operands().size() == 1,
-    	"member expression expects one operand");
+      expr.operands().size() == 1, "member expression expects one operand");
 
     return constant_propagation_reference(expr.op0());
   }
@@ -496,11 +495,10 @@ void goto_symex_statet::rename(
   else if(expr.id()==ID_address_of)
   {
     DATA_INVARIANT(
-    	expr.type().id() == ID_pointer,
-    	"type of expression required to be pointer");
+      expr.type().id() == ID_pointer,
+      "type of expression required to be pointer");
     DATA_INVARIANT(
-    	expr.operands().size() == 1,
-    	"address_of should have a single operand");
+      expr.operands().size() == 1, "address_of should have a single operand");
     rename_address(expr.op0(), ns, level);
     expr.type().subtype()=expr.op0().type();
   }

src/goto-symex/partial_order_concurrency.cpp

@@ -142,7 +142,7 @@ symbol_exprt partial_order_concurrencyt::clock(
   event_it event,
   axiomt axiom)
 {
-	PRECONDITION(!numbering.empty());
+  PRECONDITION(!numbering.empty());
   irep_idt identifier;
 
   if(event->is_shared_write())

src/goto-symex/slice_by_trace.cpp

@@ -80,11 +80,9 @@ void symex_slice_by_tracet::slice_by_trace(
     exprt g_copy(*i);
 
     DATA_INVARIANT(
-    	g_copy.id() == ID_symbol || 
-    	g_copy.id() == ID_not ||
-    	g_copy.id() == ID_and ||
-    	g_copy.id() == ID_constant,
-    	"guards should only be and, symbol, constant, or `not'");
+      g_copy.id() == ID_symbol || g_copy.id() == ID_not ||
+        g_copy.id() == ID_and || g_copy.id() == ID_constant,
+      "guards should only be and, symbol, constant, or `not'");
 
     if(g_copy.id()==ID_symbol || g_copy.id() == ID_not)
     {

src/goto-symex/symex_assign.cpp

@@ -57,7 +57,7 @@ void goto_symext::symex_assign(
       symex_allocate(state, lhs, side_effect_expr);
     else if(statement==ID_printf)
     {
-    	PRECONDITION(lhs.is_nil());
+      PRECONDITION(lhs.is_nil());
       symex_printf(state, side_effect_expr);
     }
     else if(statement==ID_gcc_builtin_va_arg_next)

src/goto-symex/symex_function_call.cpp

@@ -53,8 +53,9 @@ void goto_symext::parameter_assignments(
 
     const irep_idt &identifier=parameter.get_identifier();
 
-    INVARIANT(!identifier.empty(), 
-    	"function pointer parameter must have an identifier");
+    INVARIANT(
+      !identifier.empty(),
+      "function pointer parameter must have an identifier");
 
     const symbolt &symbol=ns.lookup(identifier);
     symbol_exprt lhs=symbol.symbol_expr();

src/goto-symex/symex_goto.cpp

@@ -346,8 +346,8 @@ void goto_symext::merge_goto(
 {
   // check atomic section
   INVARIANT(
-  	state.atomic_section_id == goto_state.atomic_section_id,
-  	"atomic sections differ across branches");
+    state.atomic_section_id == goto_state.atomic_section_id,
+    "atomic sections differ across branches");
 
   // do SSA phi functions
   phi_function(goto_state, state);

src/goto-symex/symex_other.cpp

@@ -137,9 +137,9 @@ void goto_symext::symex_other(
     // 3. build an assignment where the type on lhs and rhs is:
     // - array_copy: the type of the first array (even if the second is smaller)
     // - array_replace: the type of the second array (even if it is smaller)
-  	DATA_INVARIANT(
-  		code.operands().size() == 2,
-  		"expected array copy/array replace statement to have two operands");
+    DATA_INVARIANT(
+      code.operands().size() == 2,
+      "expected array copy/array replace statement to have two operands");
 
     // we need to add dereferencing for both operands
     dereference_exprt dest_array(code.op0());
@@ -188,8 +188,8 @@ void goto_symext::symex_other(
     // 3. use the type of the resulting array to construct an array_of
     // expression
     DATA_INVARIANT(
-  		code.operands().size() == 2,
-  		"expected array_set statement to have two operands");
+      code.operands().size() == 2,
+      "expected array_set statement to have two operands");
 
     // we need to add dereferencing for the first operand
     exprt array_expr = dereference_exprt(code.op0());
@@ -235,8 +235,8 @@ void goto_symext::symex_other(
     // the right-hand side is an equality over the arrays, if their types match;
     // if the types don't match the result trivially is false
     DATA_INVARIANT(
-  		code.operands().size() == 3,
-  		"expected array_equal statement to have three operands");
+      code.operands().size() == 3,
+      "expected array_equal statement to have three operands");
 
     // we need to add dereferencing for the first two
     dereference_exprt array1(code.op0());
@@ -269,8 +269,8 @@ void goto_symext::symex_other(
   else if(statement==ID_havoc_object)
   {
     DATA_INVARIANT(
-  		code.operands().size() == 1,
-  		"expected havoc_object statement to have one operand");
+      code.operands().size() == 1,
+      "expected havoc_object statement to have one operand");
 
     // we need to add dereferencing for the first operand
     dereference_exprt object(code.op0(), empty_typet());