diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index d0f544551b7..82aaa3b6f1a 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -345,16 +345,9 @@ class goto_programt 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. + // Use type() to access. To prevent malformed instructions, no non-const + // access method is provided. goto_program_instruction_typet _type; public: diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index c2cbee11381..751380b608d 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -97,17 +97,20 @@ static bool read_bin_goto_object( for(std::size_t ins_index = 0; ins_index < ins_count; ++ins_index) { goto_programt::targett itarget = f.body.add_instruction(); - goto_programt::instructiont &instruction=*itarget; - instruction.code_nonconst() = + // take copies as references into irepconverter are not stable + codet code = static_cast(irepconverter.reference_convert(in)); - instruction.source_location_nonconst() = - static_cast( - irepconverter.reference_convert(in)); - instruction.type_nonconst() = + source_locationt source_location = static_cast( + irepconverter.reference_convert(in)); + goto_program_instruction_typet instruction_type = (goto_program_instruction_typet)irepconverter.read_gb_word(in); - instruction.guard = + exprt guard = static_cast(irepconverter.reference_convert(in)); + + goto_programt::instructiont instruction{ + code, source_location, instruction_type, guard, {}}; + instruction.target_number = irepconverter.read_gb_word(in); if(instruction.is_target() && rev_target_map.insert( @@ -131,6 +134,8 @@ static bool read_bin_goto_object( // The above info is also held in the goto_functiont object, and could // be stored in the binary. } + + itarget->swap(instruction); } // Resolve targets diff --git a/unit/goto-programs/structured_trace_util.cpp b/unit/goto-programs/structured_trace_util.cpp index 47de51058df..9725a3ba1b5 100644 --- a/unit/goto-programs/structured_trace_util.cpp +++ b/unit/goto-programs/structured_trace_util.cpp @@ -10,12 +10,6 @@ Author: Diffblue #include #include -void link_edges(goto_programt::targett source, goto_programt::targett target) -{ - source->targets.push_back(target); - target->incoming_edges.insert(source); -} - source_locationt simple_location(const std::string &file, unsigned line) { source_locationt location; @@ -53,10 +47,13 @@ TEST_CASE("structured_trace_util", "[core][util][trace]") // 0 # normal_location add_instruction(basic_location, instructions); // 1 # loop_head - add_instruction(loop_head_location, instructions); + auto loop_head = add_instruction(loop_head_location, instructions); // 2: goto 1 # back_edge - const auto back_edge = add_instruction(back_edge_location, instructions); - back_edge->type_nonconst() = GOTO; + instructions.emplace_back( + goto_programt::make_goto(loop_head, back_edge_location)); + auto back_edge = std::prev(instructions.end()); + back_edge->location_number = 2; + loop_head->incoming_edges.insert(back_edge); // 3: no_location goto_programt::instructiont no_location; no_location.location_number = 3; @@ -64,9 +61,6 @@ TEST_CASE("structured_trace_util", "[core][util][trace]") // 4: no_file add_instruction(no_file_location, instructions); - link_edges( - std::next(instructions.begin(), 2), std::next(instructions.begin(), 1)); - SECTION("location-only steps") { goto_trace_stept step;