Merge pull request #6419 from tautschnig/nonconst-cleanup

Remove goto_programt::instructiont::type_nonconst

Author: tautschnig

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:

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<const codet &>(irepconverter.reference_convert(in));
-      instruction.source_location_nonconst() =
-        static_cast<const source_locationt &>(
-          irepconverter.reference_convert(in));
-      instruction.type_nonconst() =
+      source_locationt source_location = static_cast<const source_locationt &>(
+        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<const exprt &>(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

unit/goto-programs/structured_trace_util.cpp

@@ -10,12 +10,6 @@ Author: Diffblue
 #include <goto-programs/goto_trace.h>
 #include <goto-programs/structured_trace_util.h>
 
-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,20 +47,20 @@ 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;
   instructions.push_back(no_location);
   // 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;