use new goto_programt::instructiont API

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -432,7 +432,7 @@ bool remove_exceptionst::instrument_function_call(
   goto_programt::targett next_it=instr_it;
   next_it++;
 
-  code_function_callt &function_call=to_code_function_call(instr_it->code);
+  code_function_callt &function_call = instr_it->get_function_call();
   DATA_INVARIANT(
     function_call.function().id()==ID_symbol,
     "identified expected to be a symbol");
@@ -493,7 +493,7 @@ void remove_exceptionst::instrument_exceptions(
   {
     if(instr_it->is_decl())
     {
-      code_declt decl=to_code_decl(instr_it->code);
+      code_declt decl = instr_it->get_decl();
       locals.push_back(decl.symbol());
     }
     // Is it a handler push/pop or catch landing-pad?

src/assembler/remove_asm.cpp

@@ -107,9 +107,8 @@ void remove_asmt::gcc_asm_function_call(
 
   code_function_callt function_call(std::move(fkt), std::move(arguments));
 
-  goto_programt::targett call = dest.add_instruction(FUNCTION_CALL);
-  call->code = function_call;
-  call->source_location = code.source_location();
+  dest.add(
+    goto_programt::make_function_call(function_call, code.source_location()));
 
   // do we have it?
   if(!symbol_table.has_symbol(function_identifier))
@@ -157,9 +156,8 @@ void remove_asmt::msc_asm_function_call(
 
   code_function_callt function_call(fkt);
 
-  goto_programt::targett call = dest.add_instruction(FUNCTION_CALL);
-  call->code = function_call;
-  call->source_location = code.source_location();
+  dest.add(
+    goto_programt::make_function_call(function_call, code.source_location()));
 
   // do we have it?
   if(!symbol_table.has_symbol(function_identifier))
@@ -194,7 +192,7 @@ void remove_asmt::process_instruction(
   goto_programt::instructiont &instruction,
   goto_programt &dest)
 {
-  const code_asmt &code = to_code_asm(instruction.code);
+  const code_asmt &code = to_code_asm(instruction.get_other());
 
   const irep_idt &flavor = code.get_flavor();
 
@@ -271,14 +269,15 @@ void remove_asmt::process_instruction_gcc(
       goto_programt::targett ab = tmp_dest.add_instruction(ATOMIC_BEGIN);
       ab->source_location = code.source_location();
 
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
-      t->code.set(ID_WWfence, true);
-      t->code.set(ID_RRfence, true);
-      t->code.set(ID_RWfence, true);
-      t->code.set(ID_WRfence, true);
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+      code_fence.set(ID_WWfence, true);
+      code_fence.set(ID_RRfence, true);
+      code_fence.set(ID_RWfence, true);
+      code_fence.set(ID_WRfence, true);
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
     }
 
     if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
@@ -292,62 +291,67 @@ void remove_asmt::process_instruction_gcc(
     }
     else if(command == ID_sync) // Power
     {
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
-      t->code.set(ID_WWfence, true);
-      t->code.set(ID_RRfence, true);
-      t->code.set(ID_RWfence, true);
-      t->code.set(ID_WRfence, true);
-      t->code.set(ID_WWcumul, true);
-      t->code.set(ID_RWcumul, true);
-      t->code.set(ID_RRcumul, true);
-      t->code.set(ID_WRcumul, true);
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+      code_fence.set(ID_WWfence, true);
+      code_fence.set(ID_RRfence, true);
+      code_fence.set(ID_RWfence, true);
+      code_fence.set(ID_WRfence, true);
+      code_fence.set(ID_WWcumul, true);
+      code_fence.set(ID_RWcumul, true);
+      code_fence.set(ID_RRcumul, true);
+      code_fence.set(ID_WRcumul, true);
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
     }
     else if(command == ID_lwsync) // Power
     {
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
-      t->code.set(ID_WWfence, true);
-      t->code.set(ID_RRfence, true);
-      t->code.set(ID_RWfence, true);
-      t->code.set(ID_WWcumul, true);
-      t->code.set(ID_RWcumul, true);
-      t->code.set(ID_RRcumul, true);
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+      code_fence.set(ID_WWfence, true);
+      code_fence.set(ID_RRfence, true);
+      code_fence.set(ID_RWfence, true);
+      code_fence.set(ID_WWcumul, true);
+      code_fence.set(ID_RWcumul, true);
+      code_fence.set(ID_RRcumul, true);
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
     }
     else if(command == ID_isync) // Power
     {
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
       // doesn't do anything by itself,
       // needs to be combined with branch
     }
     else if(command == "dmb" || command == "dsb") // ARM
     {
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
-      t->code.set(ID_WWfence, true);
-      t->code.set(ID_RRfence, true);
-      t->code.set(ID_RWfence, true);
-      t->code.set(ID_WRfence, true);
-      t->code.set(ID_WWcumul, true);
-      t->code.set(ID_RWcumul, true);
-      t->code.set(ID_RRcumul, true);
-      t->code.set(ID_WRcumul, true);
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+      code_fence.set(ID_WWfence, true);
+      code_fence.set(ID_RRfence, true);
+      code_fence.set(ID_RWfence, true);
+      code_fence.set(ID_WRfence, true);
+      code_fence.set(ID_WWcumul, true);
+      code_fence.set(ID_RWcumul, true);
+      code_fence.set(ID_RRcumul, true);
+      code_fence.set(ID_WRcumul, true);
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
     }
     else if(command == "isb") // ARM
     {
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
       // doesn't do anything by itself,
       // needs to be combined with branch
     }
@@ -436,14 +440,15 @@ void remove_asmt::process_instruction_msc(
       goto_programt::targett ab = tmp_dest.add_instruction(ATOMIC_BEGIN);
       ab->source_location = code.source_location();
 
-      goto_programt::targett t = tmp_dest.add_instruction(OTHER);
-      t->source_location = code.source_location();
-      t->code = codet(ID_fence);
-      t->code.add_source_location() = code.source_location();
-      t->code.set(ID_WWfence, true);
-      t->code.set(ID_RRfence, true);
-      t->code.set(ID_RWfence, true);
-      t->code.set(ID_WRfence, true);
+      codet code_fence(ID_fence);
+      code_fence.add_source_location() = code.source_location();
+      code_fence.set(ID_WWfence, true);
+      code_fence.set(ID_RRfence, true);
+      code_fence.set(ID_RWfence, true);
+      code_fence.set(ID_WRfence, true);
+
+      tmp_dest.add(
+        goto_programt::make_other(code_fence, code.source_location()));
     }
 
     if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86

src/goto-analyzer/static_simplifier.cpp

@@ -95,7 +95,7 @@ bool static_simplifier(
       }
       else if(i_it->is_assign())
       {
-        code_assignt &assign=to_code_assign(i_it->code);
+        code_assignt &assign = i_it->get_assign();
 
         // Simplification needs to be aware of which side of the
         // expression it is handling as:
@@ -115,7 +115,7 @@ bool static_simplifier(
       }
       else if(i_it->is_function_call())
       {
-        code_function_callt &fcall=to_code_function_call(i_it->code);
+        code_function_callt &fcall = i_it->get_function_call();
 
         bool unchanged =
           ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns);

src/goto-analyzer/taint_analysis.cpp

@@ -73,8 +73,8 @@ void taint_analysist::instrument(
     {
     case FUNCTION_CALL:
       {
-        const code_function_callt &function_call=
-          to_code_function_call(instruction.code);
+        const code_function_callt &function_call =
+          instruction.get_function_call();
         const exprt &function=function_call.function();
 
         if(function.id()==ID_symbol)

src/goto-instrument/accelerate/accelerate.cpp

@@ -257,8 +257,8 @@ void acceleratet::make_overflow_loc(
   }
 
   goto_programt::targett t=program.insert_after(loop_header);
-  t->make_assignment();
-  t->code=code_assignt(overflow_var, false_exprt());
+  *t =
+    goto_programt::make_assignment(code_assignt(overflow_var, false_exprt()));
   t->swap(*loop_header);
   loop.insert(t);
   overflow_locs[loop_header].push_back(t);
@@ -360,8 +360,8 @@ void acceleratet::add_dirty_checks()
       it!=dirty_vars_map.end();
       ++it)
   {
-    goto_programt::instructiont assign(ASSIGN);
-    assign.code=code_assignt(it->second, false_exprt());
+    goto_programt::instructiont assign =
+      goto_programt::make_assignment(code_assignt(it->second, false_exprt()));
     program.insert_before_swap(program.instructions.begin(), assign);
   }
 
@@ -384,8 +384,8 @@ void acceleratet::add_dirty_checks()
 
       if(dirty_var!=dirty_vars_map.end())
       {
-        goto_programt::instructiont clear_flag(ASSIGN);
-        clear_flag.code=code_assignt(dirty_var->second, false_exprt());
+        goto_programt::instructiont clear_flag = goto_programt::make_assignment(
+          code_assignt(dirty_var->second, false_exprt()));
         program.insert_before_swap(it, clear_flag);
       }
     }

src/goto-instrument/count_eloc.cpp

@@ -164,7 +164,7 @@ void print_global_state_size(const goto_modelt &goto_model)
     {
       if(ins.is_assign())
       {
-        const code_assignt &code_assign = to_code_assign(ins.code);
+        const code_assignt &code_assign = ins.get_assign();
         object_descriptor_exprt ode;
         ode.build(code_assign.lhs(), ns);
 

src/goto-programs/cfg.h

@@ -288,8 +288,7 @@ void cfg_baset<T, P, I>::compute_edges_function_call(
   goto_programt::const_targett next_PC,
   entryt &entry)
 {
-  const exprt &function=
-    to_code_function_call(instruction.code).function();
+  const exprt &function = instruction.get_function_call().function();
 
   if(function.id()!=ID_symbol)
     return;
@@ -339,8 +338,7 @@ void procedure_local_cfg_baset<T, P, I>::compute_edges_function_call(
   goto_programt::const_targett next_PC,
   typename cfg_baset<T, P, I>::entryt &entry)
 {
-  const exprt &function=
-    to_code_function_call(instruction.code).function();
+  const exprt &function = instruction.get_function_call().function();
 
   if(function.id()!=ID_symbol)
     return;

src/goto-programs/goto_program.h

@@ -826,9 +826,11 @@ class goto_programt
       static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});
   }
 
-  static instructiont make_other(const codet &_code)
+  static instructiont make_other(
+    const codet &_code,
+    const source_locationt &l = source_locationt::nil())
   {
-    return instructiont(_code, source_locationt::nil(), OTHER, nil_exprt(), {});
+    return instructiont(_code, l, OTHER, nil_exprt(), {});
   }
 
   static instructiont make_decl(

src/goto-symex/symex_dead.cpp

@@ -21,7 +21,7 @@ void goto_symext::symex_dead(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  const code_deadt &code = to_code_dead(instruction.code);
+  const code_deadt &code = instruction.get_dead();
 
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.

src/goto-symex/symex_decl.cpp

@@ -23,13 +23,13 @@ void goto_symext::symex_decl(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  const codet &code = instruction.code;
+  const auto &code = instruction.get_decl();
 
   // two-operand decl not supported here
   // we handle the decl with only one operand
   PRECONDITION(code.operands().size() == 1);
 
-  symex_decl(state, to_code_decl(code).symbol());
+  symex_decl(state, code.symbol());
 }
 
 void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)

src/goto-symex/symex_function_call.cpp

@@ -447,7 +447,7 @@ void goto_symext::return_assignment(statet &state)
 
   const goto_programt::instructiont &instruction=*state.source.pc;
   PRECONDITION(instruction.is_return());
-  const code_returnt &code=to_code_return(instruction.code);
+  const code_returnt &code = instruction.get_return();
 
   target.location(state.guard.as_expr(), state.source);
 

src/goto-symex/symex_main.cpp

@@ -440,16 +440,15 @@ void goto_symext::symex_step(
 
   case ASSIGN:
     if(!state.guard.is_false())
-      symex_assign(state, to_code_assign(instruction.code));
+      symex_assign(state, instruction.get_assign());
 
     symex_transition(state);
     break;
 
   case FUNCTION_CALL:
     if(!state.guard.is_false())
     {
-      code_function_callt deref_code=
-        to_code_function_call(instruction.code);
+      code_function_callt deref_code = instruction.get_function_call();
 
       if(deref_code.lhs().is_not_nil())
         clean_expr(deref_code.lhs(), state, true);

src/goto-symex/symex_other.cpp

@@ -79,7 +79,7 @@ void goto_symext::symex_other(
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  const codet &code = instruction.code;
+  const codet &code = instruction.get_other();
 
   const irep_idt &statement=code.get_statement();