ensure goto_symex_statet::source is always set

sourcet contains an interator, and the interface explicitly allows it to be
uninitialised.  However, most parts of the code base access source.pc
without checking.

Author: Daniel Kroening

src/goto-symex/goto_symex_state.cpp

@@ -27,8 +27,9 @@ Author: Daniel Kroening, [email protected]
 
 static void get_l1_name(exprt &expr);
 
-goto_symex_statet::goto_symex_statet()
+goto_symex_statet::goto_symex_statet(const symex_targett::sourcet &_source)
   : depth(0),
+    source(_source),
     symex_target(nullptr),
     atomic_section_id(0),
     total_vccs(0),
@@ -767,11 +768,8 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
       ++stackit)
   {
     const auto &frame = *stackit;
-    if(frame.calling_location.is_set)
-    {
-      out << frame.calling_location.pc->function << " "
-          << frame.calling_location.pc->location_number << "\n";
-    }
+    out << frame.calling_location.pc->function << " "
+        << frame.calling_location.pc->location_number << "\n";
   }
 }
 

src/goto-symex/goto_symex_state.h

@@ -34,7 +34,7 @@ Author: Daniel Kroening, [email protected]
 class goto_symex_statet final
 {
 public:
-  goto_symex_statet();
+  explicit goto_symex_statet(const symex_targett::sourcet &);
   ~goto_symex_statet();
 
   /// \brief Fake "copy constructor" that initializes the `symex_target` member

src/goto-symex/symex_function_call.cpp

@@ -321,7 +321,6 @@ void goto_symext::symex_function_call_code(
   frame.loop_iterations[identifier].is_recursion=true;
   frame.loop_iterations[identifier].count++;
 
-  state.source.is_set=true;
   state.source.function = identifier;
   symex_transition(state, goto_function.body.instructions.begin(), false);
 }

src/goto-symex/symex_main.cpp

@@ -306,7 +306,8 @@ void goto_symext::symex_from_entry_point_of(
     throw unsupported_operation_exceptiont("the program has no entry point");
   }
 
-  statet state;
+  statet state(symex_targett::sourcet(
+    goto_functionst::entry_point(), start_function->body));
 
   state.run_validation_checks = symex_config.run_validation_checks;
 

src/goto-symex/symex_target_equation.cpp

@@ -694,15 +694,12 @@ void symex_target_equationt::SSA_stept::output(
   const namespacet &ns,
   std::ostream &out) const
 {
-  if(source.is_set)
-  {
-    out << "Thread " << source.thread_nr;
+  out << "Thread " << source.thread_nr;
 
-    if(source.pc->source_location.is_not_nil())
-      out << " " << source.pc->source_location << '\n';
-    else
-      out << '\n';
-  }
+  if(source.pc->source_location.is_not_nil())
+    out << " " << source.pc->source_location << '\n';
+  else
+    out << '\n';
 
   switch(type)
   {
@@ -795,15 +792,12 @@ void symex_target_equationt::SSA_stept::output(
 
 void symex_target_equationt::SSA_stept::output(std::ostream &out) const
 {
-  if(source.is_set)
-  {
-    out << "Thread " << source.thread_nr;
+  out << "Thread " << source.thread_nr;
 
-    if(source.pc->source_location.is_not_nil())
-      out << " " << source.pc->source_location << '\n';
-    else
-      out << '\n';
-  }
+  if(source.pc->source_location.is_not_nil())
+    out << " " << source.pc->source_location << '\n';
+  else
+    out << '\n';
 
   switch(type)
   {