Latest review comments addressed.

Author: NlightNFotis

src/goto-symex/precondition.cpp

@@ -109,14 +109,14 @@ void preconditiont::compute_rec(exprt &dest)
     // only do index!
     DATA_INVARIANT(
     	dest.operands().size() == 1,
-    	"address_of expression expected to have one operand at this point");
+    	"address_of expression expected to have one operand");
     compute_address_of(dest.op0());
   }
   else if(dest.id()==ID_dereference)
   {
     DATA_INVARIANT(
     	dest.operands().size() == 1,
-    	"dereference expression expected to have one operand at this point");
+    	"dereference expression expected to have one operand");
 
     const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
 

src/goto-symex/slice_by_trace.cpp

@@ -222,7 +222,7 @@ void symex_slice_by_tracet::parse_events(std::string read_line)
     eis.insert(event);
     PRECONDITION(!alphabet.empty());
     INVARIANT((alphabet.count(event) != 0) == alphabet_parity, 
-    	"trace uses symbol not in alphabet: " + event);
+    	"trace symbol must be in alphabet: " + event);
     if(vnext==std::string::npos)
       break;
     vidx=vnext;

src/goto-symex/symex_dereference.cpp

@@ -156,8 +156,8 @@ exprt goto_symext::address_arithmetic(
   else if(expr.id()==ID_dereference)
   {
   	DATA_INVARIANT(
-  		expr.operands().size() == 1,
-  		"dereference expression expected to have one operand");
+  	  expr.operands().size() == 1,
+  	  "dereference expression expected to have one operand");
     // ANSI-C guarantees &*p == p no matter what p is,
     // even if it's complete garbage
     // just grab the pointer, but be wary of further dereferencing
@@ -237,8 +237,8 @@ void goto_symext::dereference_rec(
   if(expr.id()==ID_dereference)
   {
     DATA_INVARIANT(
-    	expr.operands().size() == 1,
-    	"dereference expression expected to have one operand");
+      expr.operands().size() == 1,
+      "dereference expression expected to have one operand");
 
     bool expr_is_not_null = false;
 

src/goto-symex/symex_function_call.cpp

@@ -430,8 +430,8 @@ void goto_symext::return_assignment(statet &state)
   target.location(state.guard.as_expr(), state.source);
 
   PRECONDITION(
-  	code.operands().size() == 1 ||
-  	frame.return_value.is_nil());
+    code.operands().size() == 1 ||
+    frame.return_value.is_nil());
 
   exprt value=code.op0();
 

src/goto-symex/symex_goto.cpp

@@ -347,7 +347,7 @@ void goto_symext::merge_goto(
   // check atomic section
   INVARIANT(
     state.atomic_section_id == goto_state.atomic_section_id,
-    "atomic sections differ across branches");
+    "atomic section should be the same across branches");
 
   // do SSA phi functions
   phi_function(goto_state, state);