Some more changes.

Author: NlightNFotis

src/goto-symex/symex_assign.cpp

@@ -41,8 +41,9 @@ void goto_symext::symex_assign(
       	!side_effect_expr.operands().empty(),
       	"function call stamement expects non-empty list of side effects");
 
-      if(side_effect_expr.op0().id()!=ID_symbol)
-        throw "symex_assign: expected symbol as function";
+      DATA_INVARIANT(
+      	side_effect_expr.op0().id() == ID_symbol,
+        "expected symbol as function");
 
       const irep_idt &identifier=
         to_symbol_expr(side_effect_expr.op0()).get_identifier();
@@ -63,7 +64,7 @@ void goto_symext::symex_assign(
     else if(statement==ID_gcc_builtin_va_arg_next)
       symex_gcc_builtin_va_arg_next(state, lhs, side_effect_expr);
     else
-      throw "symex_assign: unexpected side effect: "+id2string(statement);
+      UNREACHABLE;
   }
   else
   {
@@ -313,11 +314,9 @@ void goto_symext::symex_assign_array(
 
   const exprt &lhs_array=lhs.array();
   const exprt &lhs_index=lhs.index();
-  const typet &lhs_type=ns.follow(lhs_array.type());
+  const typet &lhs_index_type=ns.follow(lhs_array.type());
 
-  if(lhs_type.id()!=ID_array)
-    throw "index must take array type operand, but got `"+
-          lhs_type.id_string()+"'";
+  PRECONDITION(lhs_index_type.id() == ID_array);
 
   #ifdef USE_UPDATE
 
@@ -326,7 +325,7 @@ void goto_symext::symex_assign_array(
   // into
   //   a'==UPDATE(a, [i], e)
 
-  update_exprt new_rhs(lhs_type);
+  update_exprt new_rhs(lhs_index_type);
   new_rhs.old()=lhs_array;
   new_rhs.designator().push_back(index_designatort(lhs_index));
   new_rhs.new_value()=rhs;
@@ -343,7 +342,7 @@ void goto_symext::symex_assign_array(
   //   a'==a WITH [i:=e]
 
   with_exprt new_rhs(lhs_array, lhs_index, rhs);
-  new_rhs.type() = lhs_type;
+  new_rhs.type() = lhs_index_type;
 
   exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
 

src/goto-symex/symex_start_thread.cpp

@@ -27,7 +27,7 @@ void goto_symext::symex_start_thread(statet &state)
 
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  INVARIANT(instruction.targets.size()==1,
+  INVARIANT(instruction.targets.size() == 1,
    "start_thread expects one target");
 
   goto_programt::const_targett thread_target=