introduce goto_programt::instructiont::type() and _nonconst()

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -228,7 +228,7 @@ void remove_exceptionst::instrument_exception_handler(
   const goto_programt::targett &instr_it,
   bool may_catch)
 {
-  PRECONDITION(instr_it->type==CATCH);
+  PRECONDITION(instr_it->type() == CATCH);
 
   if(may_catch)
   {
@@ -404,7 +404,7 @@ bool remove_exceptionst::instrument_throw(
   const remove_exceptionst::stack_catcht &stack_catch,
   const std::vector<symbol_exprt> &locals)
 {
-  PRECONDITION(instr_it->type==THROW);
+  PRECONDITION(instr_it->type() == THROW);
 
   const exprt &exc_expr =
     uncaught_exceptions_domaint::get_exception_symbol(instr_it->get_code());
@@ -416,13 +416,11 @@ bool remove_exceptionst::instrument_throw(
   symbol_exprt exc_thrown =
     get_inflight_exception_global();
 
-  // add the assignment with the appropriate cast
-  code_assignt assignment(
+  // now turn the `throw' into an assignment with the appropriate cast
+  *instr_it = goto_programt::make_assignment(
     exc_thrown,
-    typecast_exprt(exc_expr, exc_thrown.type()));
-  // now turn the `throw' into `assignment'
-  instr_it->type=ASSIGN;
-  instr_it->code_nonconst() = assignment;
+    typecast_exprt(exc_expr, exc_thrown.type()),
+    instr_it->source_location());
 
   return true;
 }
@@ -437,7 +435,7 @@ remove_exceptionst::instrument_function_call(
   const stack_catcht &stack_catch,
   const std::vector<symbol_exprt> &locals)
 {
-  PRECONDITION(instr_it->type==FUNCTION_CALL);
+  PRECONDITION(instr_it->type() == FUNCTION_CALL);
 
   // save the address of the next instruction
   goto_programt::targett next_it=instr_it;
@@ -512,7 +510,7 @@ void remove_exceptionst::instrument_exceptions(
       locals.push_back(instr_it->decl_symbol());
     }
     // Is it a handler push/pop or catch landing-pad?
-    else if(instr_it->type==CATCH)
+    else if(instr_it->type() == CATCH)
     {
       const irep_idt &statement = instr_it->get_code().get_statement();
       // Is it an exception landing pad (start of a catch block)?
@@ -584,12 +582,12 @@ void remove_exceptionst::instrument_exceptions(
       instr_it->turn_into_skip();
       did_something = true;
     }
-    else if(instr_it->type==THROW)
+    else if(instr_it->type() == THROW)
     {
       did_something = instrument_throw(
         function_identifier, goto_program, instr_it, stack_catch, locals);
     }
-    else if(instr_it->type==FUNCTION_CALL)
+    else if(instr_it->type() == FUNCTION_CALL)
     {
       instrumentation_resultt result =
         instrument_function_call(

jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

@@ -88,7 +88,7 @@ static goto_programt::const_targett interpret_classid_comparison(
 
   while(pc != program.instructions.end())
   {
-    if(pc->type == GOTO)
+    if(pc->type() == GOTO)
     {
       exprt guard = pc->guard;
       guard = resolve_classid_test(guard, actual_class_id, ns);
@@ -105,7 +105,7 @@ static goto_programt::const_targett interpret_classid_comparison(
         return pc;
       }
     }
-    else if(pc->type == SKIP)
+    else if(pc->type() == SKIP)
     {
       ++pc;
     }

jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp

@@ -19,7 +19,7 @@ Author: Diffblue Limited.
 static bool is_expected_virtualmethod_call(
   const goto_programt::instructiont &instruction)
 {
-  if(instruction.type != FUNCTION_CALL)
+  if(instruction.type() != FUNCTION_CALL)
     return false;
   const auto &called_function = instruction.call_function();
   if(!can_cast_expr<class_method_descriptor_exprt>(called_function))

jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

@@ -30,7 +30,7 @@ void check_function_call(
 
   for(const auto &target : targets)
   {
-    REQUIRE(target->type == goto_program_instruction_typet::FUNCTION_CALL);
+    REQUIRE(target->type() == goto_program_instruction_typet::FUNCTION_CALL);
     REQUIRE(target->call_function().id() == ID_symbol);
     REQUIRE(
       to_symbol_expr(target->call_function()).get_identifier() ==
@@ -69,7 +69,7 @@ SCENARIO(
           {
             // There should be two guarded GOTOs with non-constant guards. One
             // branching for class C and one for class D or O.
-            if(instruction.type == goto_program_instruction_typet::GOTO)
+            if(instruction.type() == goto_program_instruction_typet::GOTO)
             {
               if(instruction.guard.id() == ID_equal)
               {
@@ -146,7 +146,7 @@ SCENARIO(
         {
           irep_idt current_index;
 
-          while(it->type != goto_program_instruction_typet::END_FUNCTION)
+          while(it->type() != goto_program_instruction_typet::END_FUNCTION)
           {
             const source_locationt &loc = it->source_location();
             REQUIRE(loc != source_locationt::nil());
@@ -157,7 +157,7 @@ SCENARIO(
             {
               current_index = new_index;
               // instruction with a new bytecode index begins with ASSERT
-              REQUIRE(it->type == goto_program_instruction_typet::ASSERT);
+              REQUIRE(it->type() == goto_program_instruction_typet::ASSERT);
               // the assertion corresponds to a line coverage goal
               REQUIRE_FALSE(loc.get_basic_block_covered_lines().empty());
             }

src/analyses/custom_bitvector_analysis.cpp

@@ -283,7 +283,7 @@ void custom_bitvector_domaint::transform(
 
   const goto_programt::instructiont &instruction=*from;
 
-  switch(instruction.type)
+  switch(instruction.type())
   {
   case ASSIGN:
     assign_struct_rec(

src/analyses/escape_analysis.cpp

@@ -184,7 +184,7 @@ void escape_domaint::transform(
 
   const goto_programt::instructiont &instruction=*from;
 
-  switch(instruction.type)
+  switch(instruction.type())
   {
   case ASSIGN:
     {
@@ -460,7 +460,7 @@ void escape_analysist::instrument(
 
       const goto_programt::instructiont &instruction=*i_it;
 
-      if(instruction.type == ASSIGN)
+      if(instruction.type() == ASSIGN)
       {
         const exprt &assign_lhs = instruction.assign_lhs();
 
@@ -469,7 +469,7 @@ void escape_analysist::instrument(
         insert_cleanup(
           gf_entry.second, i_it, assign_lhs, cleanup_functions, false, ns);
       }
-      else if(instruction.type == DEAD)
+      else if(instruction.type() == DEAD)
       {
         const auto &dead_symbol = instruction.dead_symbol();
 

src/analyses/global_may_alias.cpp

@@ -107,7 +107,7 @@ void global_may_alias_domaint::transform(
 
   const goto_programt::instructiont &instruction=*from;
 
-  switch(instruction.type)
+  switch(instruction.type())
   {
   case ASSIGN:
   {

src/analyses/goto_rw.cpp

@@ -756,7 +756,7 @@ void goto_rw(
   goto_programt::const_targett target,
   rw_range_sett &rw_set)
 {
-  switch(target->type)
+  switch(target->type())
   {
   case NO_INSTRUCTION_TYPE:
   case INCOMPLETE_GOTO:

src/analyses/interval_domain.cpp

@@ -68,7 +68,7 @@ void interval_domaint::transform(
   locationt to{trace_to->current_location()};
 
   const goto_programt::instructiont &instruction=*from;
-  switch(instruction.type)
+  switch(instruction.type())
   {
   case DECL:
     havoc_rec(instruction.decl_symbol());

src/analyses/invariant_set_domain.cpp

@@ -25,7 +25,7 @@ void invariant_set_domaint::transform(
   locationt from_l(trace_from->current_location());
   locationt to_l(trace_to->current_location());
 
-  switch(from_l->type)
+  switch(from_l->type())
   {
   case GOTO:
     {

src/analyses/local_bitvector_analysis.cpp

@@ -266,7 +266,7 @@ void local_bitvector_analysist::build()
     auto &loc_info_src=loc_infos[loc_nr];
     auto loc_info_dest=loc_infos[loc_nr];
 
-    switch(instruction.type)
+    switch(instruction.type())
     {
     case ASSIGN:
       assign_lhs(

src/analyses/local_cfg.cpp

@@ -32,7 +32,7 @@ void local_cfgt::build(const goto_programt &goto_program)
     nodet &node=nodes[loc_nr];
     const goto_programt::instructiont &instruction=*node.t;
 
-    switch(instruction.type)
+    switch(instruction.type())
     {
     case GOTO:
       if(!instruction.get_condition().is_true())

src/analyses/local_may_alias.cpp

@@ -371,7 +371,7 @@ void local_may_aliast::build(const goto_functiont &goto_function)
     const loc_infot &loc_info_src=loc_infos[loc_nr];
     loc_infot loc_info_dest=loc_infos[loc_nr];
 
-    switch(instruction.type)
+    switch(instruction.type())
     {
     case ASSIGN:
     {

src/analyses/local_safe_pointers.cpp

@@ -108,7 +108,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
         instruction.location_number, checked_expressions);
     }
 
-    switch(instruction.type)
+    switch(instruction.type())
     {
     // Instruction types that definitely don't write anything, and therefore
     // can't store a null pointer:

src/analyses/uncaught_exceptions_analysis.cpp

@@ -67,7 +67,7 @@ void uncaught_exceptions_domaint::transform(
 {
   const goto_programt::instructiont &instruction=*from;
 
-  switch(instruction.type)
+  switch(instruction.type())
   {
   case THROW:
   {

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -36,7 +36,7 @@ void variable_sensitivity_domaint::transform(
 #endif
 
   const goto_programt::instructiont &instruction = *from;
-  switch(instruction.type)
+  switch(instruction.type())
   {
   case DECL:
   {
@@ -290,7 +290,7 @@ void variable_sensitivity_domaint::transform_function_call(
   ai_baset &ai,
   const namespacet &ns)
 {
-  PRECONDITION(from->type == FUNCTION_CALL);
+  PRECONDITION(from->type() == FUNCTION_CALL);
 
   const exprt &function = from->call_function();
 

src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

@@ -845,9 +845,7 @@ void disjunctive_polynomial_accelerationt::build_fixed()
   for(auto &instruction : fixed.instructions)
   {
     if(instruction.is_assert())
-    {
-      instruction.type = ASSUME;
-    }
+      instruction.turn_into_assume();
   }
 
   // We're only interested in paths that loop back to the loop header.

src/goto-instrument/accelerate/sat_path_enumerator.cpp

@@ -196,7 +196,7 @@ void sat_path_enumeratort::build_fixed()
   for(auto &instruction : fixed.instructions)
   {
     if(instruction.is_assert())
-      instruction.type = ASSUME;
+      instruction.turn_into_assume();
   }
 
   // We're only interested in paths that loop back to the loop header.

src/goto-instrument/contracts/contracts.cpp

@@ -261,8 +261,8 @@ void code_contractst::check_apply_loop_contracts(
   insert_before_swap_and_advance(goto_function.body, loop_end, havoc_code);
 
   // change the back edge into assume(false) or assume(guard)
-  loop_end->targets.clear();
-  loop_end->type = ASSUME;
+  loop_end->turn_into_assume();
+
   if(loop_head->is_goto())
     loop_end->set_condition(false_exprt());
   else

src/goto-instrument/cover.cpp

@@ -311,7 +311,8 @@ static void instrument_cover_goals(
           {
             successor->turn_into_skip();
           }
-          i_it->type = goto_program_instruction_typet::ASSUME;
+
+          i_it->turn_into_assume();
         }
         else
         {

src/goto-instrument/goto_program2code.cpp

@@ -138,7 +138,9 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
 {
   assert(target!=goto_program.instructions.end());
 
-  if(target->type != ASSERT && !target->source_location().get_comment().empty())
+  if(
+    target->type() != ASSERT &&
+    !target->source_location().get_comment().empty())
   {
     dest.add(code_skipt());
     dest.statements().back().add_source_location().set_comment(
@@ -158,7 +160,7 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
 
   convert_labels(target, dest);
 
-  switch(target->type)
+  switch(target->type())
   {
     case SKIP:
     case LOCATION:
@@ -764,10 +766,9 @@ bool goto_program2codet::set_block_end_points(
       continue;
 
     // compute the block that belongs to this case
-    for(goto_programt::const_targett case_end=it->case_start;
-        case_end!=goto_program.instructions.end() &&
-        case_end->type!=END_FUNCTION &&
-        case_end!=upper_bound;
+    for(goto_programt::const_targett case_end = it->case_start;
+        case_end != goto_program.instructions.end() &&
+        case_end->type() != END_FUNCTION && case_end != upper_bound;
         ++case_end)
     {
       const auto &case_end_node = dominators.get_node(case_end);

src/goto-instrument/k_induction.cpp

@@ -131,7 +131,7 @@ void k_inductiont::process_loop(
     {
       assert(t!=goto_function.body.instructions.end());
       if(t->is_assert())
-        t->type=ASSUME;
+        t->turn_into_assume();
     }
 
     // assume the loop condition has become false

src/goto-instrument/points_to.cpp

@@ -56,7 +56,7 @@ bool points_tot::transform(const cfgt::nodet &e)
   bool result=false;
   const goto_programt::instructiont &instruction=*(e.PC);
 
-  switch(instruction.type)
+  switch(instruction.type())
   {
   case SET_RETURN_VALUE:
     // TODO