Clarify comments in symex_dead

Try to make clearer what we can(not) remove from renaming maps. Also do small
cleanups of the code.

Author: tautschnig

src/goto-symex/symex_dead.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_symex.h"
 
-#include <cassert>
-
 #include <util/std_expr.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
@@ -23,9 +21,6 @@ void goto_symext::symex_dead(statet &state)
 
   const code_deadt &code = instruction.get_dead();
 
-  // We increase the L2 renaming to make these non-deterministic.
-  // We also prevent propagation of old values.
-
   ssa_exprt ssa(code.symbol());
   state.rename(ssa, ns, goto_symex_statet::L1);
 
@@ -45,13 +40,15 @@ void goto_symext::symex_dead(statet &state)
     state.value_set.assign(ssa, rhs, ns, true, false);
   }
 
-  ssa_exprt ssa_lhs=to_ssa_expr(ssa);
-  const irep_idt &l1_identifier=ssa_lhs.get_identifier();
+  const irep_idt &l1_identifier = to_ssa_expr(ssa).get_identifier();
 
-  // prevent propagation
+  // we cannot remove the object from the L1 renaming map, because L1 renaming
+  // information is not local to a path, but removing it from the propagation
+  // map is safe as 1) it is local to a path and 2) this instance can no longer
+  // appear
   state.propagation.erase(l1_identifier);
-
-  // L2 renaming
+  // increment the L2 index to ensure a merge on join points will propagate the
+  // value for branches that are still live
   auto level2_it = state.level2.current_names.find(l1_identifier);
   if(level2_it != state.level2.current_names.end())
     symex_renaming_levelt::increase_counter(level2_it);