Factor goto_symext::symex_dead

We'll use the symex_dead overload that takes a symbol expression rather than
an instruction to kill let-bound local definitions

Author: smowton

src/goto-symex/goto_symex.h

@@ -321,6 +321,10 @@ class goto_symext
   /// Symbolically execute a DEAD instruction
   /// \param state: Symbolic execution state for current instruction
   virtual void symex_dead(statet &state);
+  /// Kill a symbol, as if it had been the subject of a DEAD instruction
+  /// \param state: Symbolic execution state
+  /// \param symbol_expr: Symbol to kill
+  void symex_dead(statet &state, const symbol_exprt &symbol_expr);
   /// Symbolically execute an OTHER instruction
   /// \param state: Symbolic execution state for current instruction
   virtual void symex_other(statet &state);

src/goto-symex/symex_dead.cpp

@@ -21,8 +21,17 @@ void goto_symext::symex_dead(statet &state)
   const goto_programt::instructiont &instruction=*state.source.pc;
 
   const code_deadt &code = instruction.get_dead();
+  symex_dead(state, code.symbol());
+}
 
-  ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{code.symbol()}, ns).get();
+void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
+{
+  ssa_exprt ssa = state
+                    .rename_ssa<L1>(
+                      is_ssa_expr(symbol_expr) ? to_ssa_expr(symbol_expr)
+                                               : ssa_exprt{symbol_expr},
+                      ns)
+                    .get();
 
   const exprt fields = state.field_sensitivity.get_fields(ns, state, ssa);
   find_symbols_sett fields_set;