remove the trivial constructor from symex_targett::sourcet

sourcet contains an interator, and the current interface explicitly allows
it to be uninitialised.  However, most parts of the code base access
source.pc without checking.  This commit removes the option to leave the
source uninitialized.

Author: Daniel Kroening

src/goto-symex/symex_target.h

@@ -39,14 +39,9 @@ class symex_targett
     // The program counter is an iterator which indicates where the execution
     // is in its program sequence
     goto_programt::const_targett pc;
-    bool is_set;
-
-    sourcet() : thread_nr(0), function_id(irep_idt()), is_set(false)
-    {
-    }
 
     sourcet(const irep_idt &_function_id, goto_programt::const_targett _pc)
-      : thread_nr(0), function_id(_function_id), pc(_pc), is_set(true)
+      : thread_nr(0), function_id(_function_id), pc(_pc)
     {
     }
 
@@ -55,8 +50,7 @@ class symex_targett
       const goto_programt &_goto_program)
       : thread_nr(0),
         function_id(_function_id),
-        pc(_goto_program.instructions.begin()),
-        is_set(true)
+        pc(_goto_program.instructions.begin())
     {
     }
   };

unit/goto-symex/ssa_equation.cpp

@@ -25,10 +25,12 @@ SCENARIO("Validation of well-formed SSA steps", "[core][goto-symex][validate]")
     fun_symbol.name = fun_name;
     symbol_exprt fun_foo(fun_name, code_type);
 
+    goto_programt goto_program;
+    goto_program.add_instruction(END_FUNCTION);
     symex_target_equationt equation;
-    symex_targett::sourcet empty_source;
+    symex_targett::sourcet at_end_function(fun_name, goto_program);
     equation.SSA_steps.emplace_back(
-      empty_source, goto_trace_stept::typet::FUNCTION_RETURN);
+      at_end_function, goto_trace_stept::typet::FUNCTION_RETURN);
     auto &step = equation.SSA_steps.back();
     step.called_function = fun_name;