diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp index c02ae91bdd8..1ad46ecebd8 100644 --- a/jbmc/src/java_bytecode/replace_java_nondet.cpp +++ b/jbmc/src/java_bytecode/replace_java_nondet.cpp @@ -92,11 +92,10 @@ get_nondet_instruction_info(const goto_programt::const_targett &instr) { return nondet_instruction_infot(); } - const auto &code = to_code(instr->code); - if(code.get_statement() != ID_function_call) - { - return nondet_instruction_infot(); - } + const auto &code = instr->code; + INVARIANT( + code.get_statement() == ID_function_call, + "function_call should have ID_function_call"); const auto &function_call = to_code_function_call(code); return is_nondet_returning_object(function_call); } diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp index ce55e807979..b9fe025a203 100644 --- a/src/analyses/flow_insensitive_analysis.cpp +++ b/src/analyses/flow_insensitive_analysis.cpp @@ -40,19 +40,13 @@ exprt flow_insensitive_abstract_domain_baset::get_guard( exprt flow_insensitive_abstract_domain_baset::get_return_lhs(locationt to) const { // get predecessor of "to" - to--; if(to->is_end_function()) return static_cast(get_nil_irep()); // must be the function call - assert(to->is_function_call()); - - const code_function_callt &code= - to_code_function_call(to_code(to->code)); - - return code.lhs(); + return to_code_function_call(to->code).lhs(); } void flow_insensitive_analysis_baset::operator()( @@ -164,8 +158,7 @@ bool flow_insensitive_analysis_baset::visit( if(l->is_function_call()) { // this is a big special case - const code_function_callt &code= - to_code_function_call(to_code(l->code)); + const code_function_callt &code = to_code_function_call(l->code); changed= do_function_call_rec( @@ -213,8 +206,7 @@ bool flow_insensitive_analysis_baset::do_function_call( if(!goto_function.body_available()) { - const code_function_callt &code = - to_code_function_call(to_code(l_call->code)); + const code_function_callt &code = to_code_function_call(l_call->code); goto_programt temp; diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index a591883ad24..a2656486686 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -626,7 +626,7 @@ void c_typecheck_baset::typecheck_ifthenelse(code_ifthenelset &code) implicit_typecast_bool(cond); - if(to_code(code.then_case()).get_statement()==ID_decl_block) + if(code.then_case().get_statement() == ID_decl_block) { code_blockt code_block; code_block.add_source_location()=code.then_case().source_location(); @@ -635,11 +635,11 @@ void c_typecheck_baset::typecheck_ifthenelse(code_ifthenelset &code) code.then_case().swap(code_block); } - typecheck_code(to_code(code.then_case())); + typecheck_code(code.then_case()); if(!code.else_case().is_nil()) { - if(to_code(code.else_case()).get_statement()==ID_decl_block) + if(code.else_case().get_statement() == ID_decl_block) { code_blockt code_block; code_block.add_source_location()=code.else_case().source_location(); @@ -648,7 +648,7 @@ void c_typecheck_baset::typecheck_ifthenelse(code_ifthenelset &code) code.else_case().swap(code_block); } - typecheck_code(to_code(code.else_case())); + typecheck_code(code.else_case()); } } diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index d1bf4d069e5..2f91ac42e00 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -2593,9 +2593,9 @@ std::string expr2ct::convert_code_ifthenelse( dest+=';'; } else - dest+=convert_code( - to_code(src.then_case()), - to_code(src.then_case()).get_statement()==ID_block ? indent : indent+2); + dest += convert_code( + src.then_case(), + src.then_case().get_statement() == ID_block ? indent : indent + 2); dest+="\n"; if(!src.else_case().is_nil()) @@ -2603,9 +2603,9 @@ std::string expr2ct::convert_code_ifthenelse( dest+="\n"; dest+=indent_str(indent); dest+="else\n"; - dest+=convert_code( - to_code(src.else_case()), - to_code(src.else_case()).get_statement()==ID_block ? indent : indent+2); + dest += convert_code( + src.else_case(), + src.else_case().get_statement() == ID_block ? indent : indent + 2); } return dest; diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 9694c2781d1..5f8a4b00c74 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1117,17 +1117,17 @@ goto_programt::const_targett goto_program2codet::convert_goto_if( if(has_else) { for(++target; target!=before_else; ++target) - target=convert_instruction(target, before_else, to_code(i.then_case())); + target = convert_instruction(target, before_else, i.then_case()); - convert_labels(before_else, to_code(i.then_case())); + convert_labels(before_else, i.then_case()); for(++target; target!=end_if; ++target) - target=convert_instruction(target, end_if, to_code(i.else_case())); + target = convert_instruction(target, end_if, i.else_case()); } else { for(++target; target!=end_if; ++target) - target=convert_instruction(target, end_if, to_code(i.then_case())); + target = convert_instruction(target, end_if, i.then_case()); } dest.move_to_operands(i); @@ -1354,12 +1354,12 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( // use pthreads if "code in new thread" is a function call to a function with // suitable signature - if(thread_start->is_function_call() && - to_code_function_call(to_code(thread_start->code)).arguments().size()==1 && - after_thread_start==thread_end) + if( + thread_start->is_function_call() && + to_code_function_call(thread_start->code).arguments().size() == 1 && + after_thread_start == thread_end) { - const code_function_callt &cf= - to_code_function_call(to_code(thread_start->code)); + const code_function_callt &cf = to_code_function_call(thread_start->code); system_headers.insert("pthread.h"); @@ -1730,14 +1730,15 @@ void goto_program2codet::cleanup_code_ifthenelse( // assert(false) expands to if(true) assert(false), simplify again (and also // simplify other cases) - if(cond.is_true() && - (i_t_e.else_case().is_nil() || !has_labels(to_code(i_t_e.else_case())))) + if( + cond.is_true() && + (i_t_e.else_case().is_nil() || !has_labels(i_t_e.else_case()))) { codet tmp; tmp.swap(i_t_e.then_case()); code.swap(tmp); } - else if(cond.is_false() && !has_labels(to_code(i_t_e.then_case()))) + else if(cond.is_false() && !has_labels(i_t_e.then_case())) { if(i_t_e.else_case().is_nil()) code=code_skipt(); @@ -1750,8 +1751,9 @@ void goto_program2codet::cleanup_code_ifthenelse( } else { - if(i_t_e.then_case().is_not_nil() && - to_code(i_t_e.then_case()).get_statement()==ID_ifthenelse) + if( + i_t_e.then_case().is_not_nil() && + i_t_e.then_case().get_statement() == ID_ifthenelse) { // we re-introduce 1-code blocks with if-then-else to avoid dangling-else // ambiguity @@ -1760,9 +1762,10 @@ void goto_program2codet::cleanup_code_ifthenelse( i_t_e.then_case().swap(b); } - if(i_t_e.else_case().is_not_nil() && - to_code(i_t_e.then_case()).get_statement()==ID_skip && - to_code(i_t_e.else_case()).get_statement()==ID_ifthenelse) + if( + i_t_e.else_case().is_not_nil() && + i_t_e.then_case().get_statement() == ID_skip && + i_t_e.else_case().get_statement() == ID_ifthenelse) { // we re-introduce 1-code blocks with if-then-else to avoid dangling-else // ambiguity @@ -1795,8 +1798,9 @@ void goto_program2codet::cleanup_code_ifthenelse( } // remove empty then/else - if(code.get_statement()==ID_ifthenelse && - to_code(i_t_e.then_case()).get_statement()==ID_skip) + if( + code.get_statement() == ID_ifthenelse && + i_t_e.then_case().get_statement() == ID_skip) { not_exprt tmp(i_t_e.cond()); simplify(tmp, ns); @@ -1805,15 +1809,15 @@ void goto_program2codet::cleanup_code_ifthenelse( i_t_e.cond().swap(tmp); i_t_e.then_case().swap(i_t_e.else_case()); } - if(code.get_statement()==ID_ifthenelse && - i_t_e.else_case().is_not_nil() && - to_code(i_t_e.else_case()).get_statement()==ID_skip) + if( + code.get_statement() == ID_ifthenelse && i_t_e.else_case().is_not_nil() && + i_t_e.else_case().get_statement() == ID_skip) i_t_e.else_case().make_nil(); // or even remove the if altogether if the then case is now empty - if(code.get_statement()==ID_ifthenelse && - i_t_e.else_case().is_nil() && - (i_t_e.then_case().is_nil() || - to_code(i_t_e.then_case()).get_statement()==ID_skip)) + if( + code.get_statement() == ID_ifthenelse && i_t_e.else_case().is_nil() && + (i_t_e.then_case().is_nil() || + i_t_e.then_case().get_statement() == ID_skip)) code=code_skipt(); } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index a2a626f38dd..b9259cbe9a6 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -1569,12 +1569,12 @@ void goto_convertt::convert_ifthenelse( // convert 'then'-branch goto_programt tmp_then; - convert(to_code(code.then_case()), tmp_then, mode); + convert(code.then_case(), tmp_then, mode); goto_programt tmp_else; if(has_else) - convert(to_code(code.else_case()), tmp_else, mode); + convert(code.else_case(), tmp_else, mode); exprt tmp_guard=code.cond(); clean_expr(tmp_guard, dest, mode); diff --git a/src/goto-programs/remove_unused_functions.cpp b/src/goto-programs/remove_unused_functions.cpp index fbb4d9d5947..85cb1e3364c 100644 --- a/src/goto-programs/remove_unused_functions.cpp +++ b/src/goto-programs/remove_unused_functions.cpp @@ -75,8 +75,7 @@ void find_used_functions( { if(it->type==FUNCTION_CALL) { - const code_function_callt &call = - to_code_function_call(to_code(it->code)); + const code_function_callt &call = to_code_function_call(it->code); // check that this is actually a simple call assert(call.function().id()==ID_symbol); diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp index 8bf28a28813..32551d53bc1 100644 --- a/src/goto-symex/memory_model_tso.cpp +++ b/src/goto-symex/memory_model_tso.cpp @@ -107,7 +107,7 @@ void memory_model_tsot::program_order( if((*e_it2)->is_memory_barrier()) { - const codet &code=to_code((*e_it2)->source.pc->code); + const codet &code = (*e_it2)->source.pc->code; if((*e_it)->is_shared_read() && !code.get_bool(ID_RRfence) && diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index a6654c99409..ee6c582bf5f 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/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 codet &code=to_code(instruction.code); + const codet &code = instruction.code; if(code.operands().size()!=1) throw "dead expects one operand"; diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index 776f8ddd2ed..2961684a3fc 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -23,7 +23,7 @@ void goto_symext::symex_decl(statet &state) { const goto_programt::instructiont &instruction=*state.source.pc; - const codet &code=to_code(instruction.code); + const codet &code = instruction.code; if(code.operands().size()==2) throw "two-operand decl not supported here"; diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index c1ceff5c12d..b6f62d2dcd6 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -78,7 +78,7 @@ void goto_symext::symex_other( { const goto_programt::instructiont &instruction=*state.source.pc; - const codet &code=to_code(instruction.code); + const codet &code = instruction.code; const irep_idt &statement=code.get_statement(); diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index 36393c73af6..f0628ea8a0e 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -832,10 +832,10 @@ void jsil_typecheckt::typecheck_ifthenelse(code_ifthenelset &code) typecheck_expr(cond); make_type_compatible(cond, bool_typet(), true); - typecheck_code(to_code(code.then_case())); + typecheck_code(code.then_case()); if(!code.else_case().is_nil()) - typecheck_code(to_code(code.else_case())); + typecheck_code(code.else_case()); } void jsil_typecheckt::typecheck_assign(code_assignt &code) diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp index 063af881e52..f8a395f5246 100644 --- a/src/pointer-analysis/goto_program_dereference.cpp +++ b/src/pointer-analysis/goto_program_dereference.cpp @@ -307,7 +307,7 @@ void goto_program_dereferencet::dereference_instruction( } else if(i.is_function_call()) { - code_function_callt &function_call=to_code_function_call(to_code(i.code)); + code_function_callt &function_call = to_code_function_call(i.code); if(function_call.lhs().is_not_nil()) dereference_expr(