Remove dead symbols from assignable set

Author: SaswatPadhi

src/goto-instrument/contracts/assigns.cpp

@@ -110,6 +110,11 @@ void assigns_clauset::add_target(const exprt &target_expr)
   }
 }
 
+void assigns_clauset::remove_target(const exprt &target_expr)
+{
+  targets.erase(targett(*this, targett::normalize(target_expr)));
+}
+
 goto_programt assigns_clauset::generate_havoc_code() const
 {
   modifiest modifies;

src/goto-instrument/contracts/assigns.h

@@ -54,6 +54,7 @@ class assigns_clauset
   assigns_clauset(const exprt &, const messaget &, const namespacet &);
 
   void add_target(const exprt &);
+  void remove_target(const exprt &);
 
   goto_programt generate_havoc_code() const;
   exprt generate_containment_check(const exprt &) const;

src/goto-instrument/contracts/contracts.cpp

@@ -944,6 +944,13 @@ void code_contractst::check_frame_conditions(
         freely_assignable_symbols,
         assigns);
     }
+    else if(instruction_it->is_dead())
+    {
+      freely_assignable_symbols.erase(
+        instruction_it->get_dead().symbol().get_identifier());
+
+      assigns.remove_target(instruction_it->get_dead().symbol());
+    }
   }
 }