diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index 250ed5fc29a..e237ba82eb0 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/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 &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 &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( diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp index 04081041392..65af2b36fe9 100644 --- a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp +++ b/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; } diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp index 63eca24f78e..a0636862d0a 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp +++ b/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(called_function)) diff --git a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp index d41cdfb8f03..ab445cbebc3 100644 --- a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp +++ b/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()); } diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 2f0d28a70d6..231a48fe2ca 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/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( diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index d750c98470a..5fdb9a2d1c6 100644 --- a/src/analyses/escape_analysis.cpp +++ b/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(); diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 1d86316fd55..47b1dcb40b9 100644 --- a/src/analyses/global_may_alias.cpp +++ b/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: { diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 19dd6c8e80d..cf727b3f57d 100644 --- a/src/analyses/goto_rw.cpp +++ b/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: diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index ebfb073efd6..a8a4038f6d1 100644 --- a/src/analyses/interval_domain.cpp +++ b/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()); diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp index aed7e17db41..03f3df8bbf8 100644 --- a/src/analyses/invariant_set_domain.cpp +++ b/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: { diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index c897d91f658..338f8051ae6 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/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( diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp index 92de012b634..42bb6d8e3de 100644 --- a/src/analyses/local_cfg.cpp +++ b/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()) diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index 058aee388c9..200916d58e9 100644 --- a/src/analyses/local_may_alias.cpp +++ b/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: { diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp index 58aa2a66880..3bb53eff009 100644 --- a/src/analyses/local_safe_pointers.cpp +++ b/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: diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index 9fac2fbd4fd..b851b72d403 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/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: { diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index 62c555d4cfd..d6bff1f151d 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/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(); diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index 50bf969db5a..d0a28fbb6bb 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/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. diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp index 053021e998c..28c3963995f 100644 --- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp +++ b/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. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 9ce1c1d33d1..6b1724a4c4f 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/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 diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index bb0d43999b2..99d9d03dc1c 100644 --- a/src/goto-instrument/cover.cpp +++ b/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 { diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 4387e957af3..88f55491a5c 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/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); diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp index a66b8a47a17..db11ec8425f 100644 --- a/src/goto-instrument/k_induction.cpp +++ b/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 diff --git a/src/goto-instrument/points_to.cpp b/src/goto-instrument/points_to.cpp index d3f32f4e13a..a14b4a91898 100644 --- a/src/goto-instrument/points_to.cpp +++ b/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 diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index da30c02011b..d22f8a400ed 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -112,21 +112,20 @@ void uninitializedt::add_assertions( if(tracking.find(identifier)!=tracking.end()) { - goto_programt::targett i1=goto_program.insert_after(i_it); - goto_programt::targett i2=goto_program.insert_after(i1); - i_it++, i_it++; - const irep_idt new_identifier= id2string(identifier)+"#initialized"; symbol_exprt symbol_expr(new_identifier, bool_typet()); - i1->type=DECL; - i1->source_location_nonconst() = instruction.source_location(); - i1->code_nonconst() = code_declt(symbol_expr); + goto_programt::instructiont i1 = + goto_programt::make_decl(symbol_expr, instruction.source_location()); + + goto_programt::instructiont i2 = goto_programt::make_assignment( + symbol_expr, false_exprt(), instruction.source_location()); - i2->type=ASSIGN; - i2->source_location_nonconst() = instruction.source_location(); - i2->code_nonconst() = code_assignt(symbol_expr, false_exprt()); + goto_programt::targett i1_it = + goto_program.insert_after(i_it, std::move(i1)); + goto_program.insert_after(i1_it, std::move(i2)); + i_it++, i_it++; } } else @@ -180,12 +179,11 @@ void uninitializedt::add_assertions( { const irep_idt new_identifier=id2string(identifier)+"#initialized"; - goto_programt::instructiont assignment; - assignment.type=ASSIGN; - assignment.code_nonconst() = code_assignt( - symbol_exprt(new_identifier, bool_typet()), true_exprt()); - assignment.source_location_nonconst() = - instruction.source_location(); + goto_programt::instructiont assignment = + goto_programt::make_assignment( + symbol_exprt(new_identifier, bool_typet()), + true_exprt(), + instruction.source_location()); goto_program.insert_before_swap(i_it, assignment); i_it++; diff --git a/src/goto-instrument/value_set_fi_fp_removal.cpp b/src/goto-instrument/value_set_fi_fp_removal.cpp index 1d2f3e46f6a..2844c20c3d6 100644 --- a/src/goto-instrument/value_set_fi_fp_removal.cpp +++ b/src/goto-instrument/value_set_fi_fp_removal.cpp @@ -175,10 +175,8 @@ void remove_function_pointer( // We preserve the original dereferencing to possibly catch // further pointer-related errors. - code_expressiont code_expression(function); - code_expression.add_source_location() = function.source_location(); - target->code_nonconst().swap(code_expression); - target->type = OTHER; + *target = goto_programt::make_other( + code_expressiont(function), function.source_location()); } void value_set_fi_fp_removal( diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 26240fd784b..19e941cf308 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -186,8 +186,8 @@ void instrumentert::cfg_visitort::visit_cfg_function( current_thread=coming_from; thread=current_thread; - instrumenter.message.debug() << "visit instruction "<type=ASSIGN; - t->code_nonconst() = code_assignt(symbol, value); - t->code_nonconst().add_source_location() = source_location; - t->source_location_nonconst() = source_location; + t = goto_program.insert_before( + t, goto_programt::make_assignment(symbol, value, source_location)); // instrumentations.insert((const irep_idt) (t->code.id())); @@ -1072,8 +1069,8 @@ void shared_bufferst::cfg_visitort::weak_memory( { goto_programt::instructiont &instruction=*i_it; - shared_buffers.message.debug() << "instruction "<::compute_edges( next_PC++; // compute forward edges first - switch(instruction.type) + switch(instruction.type()) { case GOTO: compute_edges_goto(goto_program, instruction, next_PC, entry); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 17e9ed098c8..dbbd5e226dc 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -208,8 +208,8 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program) const exprt pointer = destination.pointer(); // remember the expression for later checks - i.type=OTHER; - i.code_nonconst() = code_expressiont(pointer); + i = + goto_programt::make_other(code_expressiont(pointer), i.source_location()); // insert huge case-split for(const auto &label : targets.labels) diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 142d375fa2b..a7536ffccda 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -162,15 +162,15 @@ void goto_inlinet::replace_return( { // a typecast may be necessary if the declared return type at the call // site differs from the defined return type - it->code_nonconst() = code_assignt( + *it = goto_programt::make_assignment( lhs, - typecast_exprt::conditional_cast(it->return_value(), lhs.type())); - it->type=ASSIGN; + typecast_exprt::conditional_cast(it->return_value(), lhs.type()), + it->source_location()); } else { - it->code_nonconst() = code_expressiont(it->return_value()); - it->type=OTHER; + *it = goto_programt::make_other( + code_expressiont(it->return_value()), it->source_location()); } } } @@ -232,7 +232,7 @@ void goto_inlinet::insert_function_body( DATA_INVARIANT( end.is_end_function(), "final instruction of a function must be an END_FUNCTION"); - end.type=LOCATION; + end = goto_programt::make_location(end.source_location()); // make sure the inlined function does not introduce hiding if(goto_function.is_hidden()) @@ -290,8 +290,7 @@ void goto_inlinet::insert_function_body( } // kill call - target->type=LOCATION; - target->code_nonconst().clear(); + *target = goto_programt::make_location(target->source_location()); target++; dest.destructive_insert(target, tmp); diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 617cdec5666..11bbef61ebf 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -83,7 +83,7 @@ std::ostream &goto_programt::output_instruction( else out << " "; - switch(instruction.type) + switch(instruction.type()) { case NO_INSTRUCTION_TYPE: out << "NO INSTRUCTION TYPE SET" << '\n'; @@ -331,7 +331,7 @@ std::list expressions_read( { std::list dest; - switch(instruction.type) + switch(instruction.type()) { case ASSUME: case ASSERT: @@ -380,7 +380,7 @@ std::list expressions_written( { std::list dest; - switch(instruction.type) + switch(instruction.type()) { case FUNCTION_CALL: if(instruction.call_lhs().is_not_nil()) @@ -486,7 +486,7 @@ std::string as_string( { std::string result; - switch(i.type) + switch(i.type()) { case NO_INSTRUCTION_TYPE: return "(NO INSTRUCTION TYPE)"; @@ -743,7 +743,7 @@ bool goto_programt::instructiont::equals(const instructiont &other) const { // clang-format off return - type == other.type && + _type == other._type && code == other.code && guard == other.guard && targets.size() == other.targets.size() && @@ -842,7 +842,7 @@ void goto_programt::instructiont::validate( }; const symbolt *table_symbol; - switch(type) + switch(_type) { case NO_INSTRUCTION_TYPE: break; @@ -955,7 +955,7 @@ void goto_programt::instructiont::validate( void goto_programt::instructiont::transform( std::function(exprt)> f) { - switch(type) + switch(_type) { case OTHER: if(get_other().get_statement() == ID_expression) @@ -1059,7 +1059,7 @@ void goto_programt::instructiont::transform( void goto_programt::instructiont::apply( std::function f) const { - switch(type) + switch(_type) { case OTHER: if(get_other().get_statement() == ID_expression) diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 904a6f3e5b3..d0f544551b7 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -340,8 +340,24 @@ class goto_programt } /// What kind of instruction? - goto_program_instruction_typet type; + goto_program_instruction_typet type() const + { + return _type; + } + + /// Set the kind of the instruction. + /// This method is best avoided to prevent mal-formed instructions. + /// Consider using the goto_programt::make_X methods instead. + goto_program_instruction_typet &type_nonconst() + { + return _type; + } + + protected: + // Use type() and type_nonconst() to access. + goto_program_instruction_typet _type; + public: /// Guard for gotos, assume, assert /// Use condition() method to access. /// This member will eventually be protected. @@ -426,9 +442,9 @@ class goto_programt { return target_number!=nil_target; } /// Clear the node - void clear(goto_program_instruction_typet _type) + void clear(goto_program_instruction_typet __type) { - type=_type; + _type = __type; targets.clear(); guard=true_exprt(); code.make_nil(); @@ -441,34 +457,44 @@ class goto_programt clear(SKIP); } + /// Transforms either an assertion or a GOTO instruction + /// into an assumption, with the same condition. + void turn_into_assume() + { + PRECONDITION(_type == GOTO || _type == ASSERT); + _type = ASSUME; + targets.clear(); + code.make_nil(); + } + void complete_goto(targett _target) { - PRECONDITION(type == INCOMPLETE_GOTO); + PRECONDITION(_type == INCOMPLETE_GOTO); code.make_nil(); targets.push_back(_target); - type = GOTO; + _type = GOTO; } // clang-format off - bool is_goto () const { return type == GOTO; } - bool is_set_return_value() const { return type == SET_RETURN_VALUE; } - bool is_assign () const { return type == ASSIGN; } - bool is_function_call () const { return type == FUNCTION_CALL; } - bool is_throw () const { return type == THROW; } - bool is_catch () const { return type == CATCH; } - bool is_skip () const { return type == SKIP; } - bool is_location () const { return type == LOCATION; } - bool is_other () const { return type == OTHER; } - bool is_decl () const { return type == DECL; } - bool is_dead () const { return type == DEAD; } - bool is_assume () const { return type == ASSUME; } - bool is_assert () const { return type == ASSERT; } - bool is_atomic_begin () const { return type == ATOMIC_BEGIN; } - bool is_atomic_end () const { return type == ATOMIC_END; } - bool is_start_thread () const { return type == START_THREAD; } - bool is_end_thread () const { return type == END_THREAD; } - bool is_end_function () const { return type == END_FUNCTION; } - bool is_incomplete_goto () const { return type == INCOMPLETE_GOTO; } + bool is_goto () const { return _type == GOTO; } + bool is_set_return_value() const { return _type == SET_RETURN_VALUE; } + bool is_assign () const { return _type == ASSIGN; } + bool is_function_call () const { return _type == FUNCTION_CALL; } + bool is_throw () const { return _type == THROW; } + bool is_catch () const { return _type == CATCH; } + bool is_skip () const { return _type == SKIP; } + bool is_location () const { return _type == LOCATION; } + bool is_other () const { return _type == OTHER; } + bool is_decl () const { return _type == DECL; } + bool is_dead () const { return _type == DEAD; } + bool is_assume () const { return _type == ASSUME; } + bool is_assert () const { return _type == ASSERT; } + bool is_atomic_begin () const { return _type == ATOMIC_BEGIN; } + bool is_atomic_end () const { return _type == ATOMIC_END; } + bool is_start_thread () const { return _type == START_THREAD; } + bool is_end_thread () const { return _type == END_THREAD; } + bool is_end_function () const { return _type == END_FUNCTION; } + bool is_incomplete_goto () const { return _type == INCOMPLETE_GOTO; } // clang-format on instructiont(): @@ -476,10 +502,10 @@ class goto_programt { } - explicit instructiont(goto_program_instruction_typet _type) + explicit instructiont(goto_program_instruction_typet __type) : code(static_cast(get_nil_irep())), _source_location(static_cast(get_nil_irep())), - type(_type), + _type(__type), guard(true_exprt()) { } @@ -488,12 +514,12 @@ class goto_programt instructiont( codet _code, source_locationt __source_location, - goto_program_instruction_typet _type, + goto_program_instruction_typet __type, exprt _guard, targetst _targets) : code(std::move(_code)), _source_location(std::move(__source_location)), - type(_type), + _type(__type), guard(std::move(_guard)), targets(std::move(_targets)) { @@ -505,7 +531,7 @@ class goto_programt using std::swap; swap(instruction.code, code); swap(instruction._source_location, _source_location); - swap(instruction.type, type); + swap(instruction._type, _type); swap(instruction.guard, guard); swap(instruction.targets, targets); } @@ -542,7 +568,7 @@ class goto_programt std::string to_string() const { std::ostringstream instruction_id_builder; - instruction_id_builder << type; + instruction_id_builder << _type; return instruction_id_builder.str(); } diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 597c300b5fd..85140c26ad7 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -115,7 +115,7 @@ void goto_trace_stept::output( if(!pc->source_location().is_nil()) out << pc->source_location() << '\n'; - out << pc->type << '\n'; + out << pc->type() << '\n'; if(pc->is_assert()) { diff --git a/src/goto-programs/instrument_preconditions.cpp b/src/goto-programs/instrument_preconditions.cpp index ecbc70168be..10c4409f2dc 100644 --- a/src/goto-programs/instrument_preconditions.cpp +++ b/src/goto-programs/instrument_preconditions.cpp @@ -62,7 +62,7 @@ void remove_preconditions(goto_programt &goto_program) instruction.is_assert() && instruction.source_location().get_property_class() == ID_precondition) { - instruction.type=LOCATION; + instruction = goto_programt::make_location(instruction.source_location()); } else break; // preconditions must be at the front diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 19ca44b708b..a4e73e46195 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -258,7 +258,7 @@ void interpretert::step() goto_trace_stept &trace_step=steps.get_last_step(); trace_step.thread_nr=thread_id; trace_step.pc=pc; - switch(pc->type) + switch(pc->type()) { case GOTO: trace_step.type=goto_trace_stept::typet::GOTO; @@ -337,7 +337,7 @@ void interpretert::step() break; case THROW: trace_step.type=goto_trace_stept::typet::GOTO; - while(!done && (pc->type!=CATCH)) + while(!done && (pc->type() != CATCH)) { if(pc==function->second.body.instructions.end()) { diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 5c2326eb476..c2cbee11381 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -104,8 +104,8 @@ static bool read_bin_goto_object( instruction.source_location_nonconst() = static_cast( irepconverter.reference_convert(in)); - instruction.type = (goto_program_instruction_typet) - irepconverter.read_gb_word(in); + instruction.type_nonconst() = + (goto_program_instruction_typet)irepconverter.read_gb_word(in); instruction.guard = static_cast(irepconverter.reference_convert(in)); instruction.target_number = irepconverter.read_gb_word(in); diff --git a/src/goto-programs/remove_calls_no_body.cpp b/src/goto-programs/remove_calls_no_body.cpp index ea61c6dac10..857d04d1f37 100644 --- a/src/goto-programs/remove_calls_no_body.cpp +++ b/src/goto-programs/remove_calls_no_body.cpp @@ -52,8 +52,7 @@ void remove_calls_no_bodyt::remove_call_no_body( } // kill call - target->type = LOCATION; - target->code_nonconst().clear(); + *target = goto_programt::make_location(target->source_location()); target++; goto_program.destructive_insert(target, tmp); diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index b2714d5bf59..e4903f8d9ee 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -446,8 +446,8 @@ void remove_function_pointerst::remove_function_pointer( // further pointer-related errors. code_expressiont code_expression(function); code_expression.add_source_location()=function.source_location(); - target->code_nonconst().swap(code_expression); - target->type=OTHER; + *target = + goto_programt::make_other(code_expression, target->source_location()); // report statistics log.statistics().source_location = target->source_location(); diff --git a/src/goto-programs/remove_unused_functions.cpp b/src/goto-programs/remove_unused_functions.cpp index 0128702c90b..17a8cec60db 100644 --- a/src/goto-programs/remove_unused_functions.cpp +++ b/src/goto-programs/remove_unused_functions.cpp @@ -73,7 +73,7 @@ void find_used_functions( { for(const auto &instruction : f_it->second.body.instructions) { - if(instruction.type == FUNCTION_CALL) + if(instruction.is_function_call()) { const auto &function = instruction.call_function(); diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 45d705c349b..6995a315d46 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -153,12 +153,12 @@ static goto_programt analyse_checks_directly_preceding_function_call( { instr_it = std::prev(instr_it); - if(instr_it->type == ASSERT) + if(instr_it->is_assert()) { continue; } - if(instr_it->type != ASSUME) + if(!instr_it->is_assume()) { break; } diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 5e38f84e07e..f4cbf286136 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -465,7 +465,7 @@ goto_programt::targett string_abstractiont::abstract( goto_programt &dest, goto_programt::targett it) { - switch(it->type) + switch(it->type()) { case ASSIGN: it=abstract_assign(dest, it); diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp index 43c16d7fcdd..4355bc3c459 100644 --- a/src/goto-programs/write_goto_binary.cpp +++ b/src/goto-programs/write_goto_binary.cpp @@ -97,7 +97,7 @@ bool write_goto_binary( { irepconverter.reference_convert(instruction.get_code(), out); irepconverter.reference_convert(instruction.source_location(), out); - write_gb_word(out, (long)instruction.type); + write_gb_word(out, (long)instruction.type()); const auto condition = instruction.has_condition() ? instruction.condition() : true_exprt(); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 92a9c8547f3..36cd1b1a55b 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -516,9 +516,9 @@ void goto_symext::print_symex_step(statet &state) // debugging and if there's no code block at this point. if( !symex_config.show_symex_steps || !state.reachable || - state.source.pc->type == DEAD || + state.source.pc->type() == DEAD || (state.source.pc->get_code().is_nil() && - state.source.pc->type != END_FUNCTION)) + state.source.pc->type() != END_FUNCTION)) { return; } @@ -551,7 +551,7 @@ void goto_symext::print_symex_step(statet &state) // Print the method we're returning too. const auto &call_stack = state.threads[state.source.thread_nr].call_stack; - if(state.source.pc->type == END_FUNCTION) + if(state.source.pc->type() == END_FUNCTION) { log.status() << messaget::eom; @@ -566,7 +566,7 @@ void goto_symext::print_symex_step(statet &state) } // On a function call print the entire call stack. - if(state.source.pc->type == FUNCTION_CALL) + if(state.source.pc->type() == FUNCTION_CALL) { log.status() << messaget::eom; @@ -620,7 +620,7 @@ void goto_symext::execute_next_instruction( state.depth++; // actually do instruction - switch(instruction.type) + switch(instruction.type()) { case SKIP: if(state.reachable) diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h index 6c8c3c445d5..a256718694f 100644 --- a/src/pointer-analysis/value_set_domain.h +++ b/src/pointer-analysis/value_set_domain.h @@ -70,7 +70,7 @@ void value_set_domain_templatet::transform( const irep_idt &function_to, locationt to_l) { - switch(from_l->type) + switch(from_l->type()) { case GOTO: // ignore for now diff --git a/src/pointer-analysis/value_set_domain_fi.cpp b/src/pointer-analysis/value_set_domain_fi.cpp index d78abdb2184..eaff53f58fc 100644 --- a/src/pointer-analysis/value_set_domain_fi.cpp +++ b/src/pointer-analysis/value_set_domain_fi.cpp @@ -30,7 +30,7 @@ bool value_set_domain_fit::transform( // from_l->function << " " << from_l->location_number << " to " << // to_l->function << " " << to_l->location_number << '\n'; - switch(from_l->type) + switch(from_l->type()) { case GOTO: // ignore for now diff --git a/src/solvers/solver_hardness.cpp b/src/solvers/solver_hardness.cpp index e43992a7925..de589f814e7 100644 --- a/src/solvers/solver_hardness.cpp +++ b/src/solvers/solver_hardness.cpp @@ -236,7 +236,7 @@ solver_hardnesst::goto_instruction2string(goto_programt::const_targett pc) if(instruction.is_target()) out << std::setw(6) << instruction.target_number << ": "; - switch(instruction.type) + switch(instruction.type()) { case NO_INSTRUCTION_TYPE: out << "NO INSTRUCTION TYPE SET"; diff --git a/unit/goto-programs/structured_trace_util.cpp b/unit/goto-programs/structured_trace_util.cpp index 80273dce885..47de51058df 100644 --- a/unit/goto-programs/structured_trace_util.cpp +++ b/unit/goto-programs/structured_trace_util.cpp @@ -56,7 +56,7 @@ TEST_CASE("structured_trace_util", "[core][util][trace]") add_instruction(loop_head_location, instructions); // 2: goto 1 # back_edge const auto back_edge = add_instruction(back_edge_location, instructions); - back_edge->type = GOTO; + back_edge->type_nonconst() = GOTO; // 3: no_location goto_programt::instructiont no_location; no_location.location_number = 3;