Merge pull request #5869 from hannes-steffenhagen-diffblue/fix/constant-propagator-bug

Fix bug in constant propagator

Author: hannes-steffenhagen-diffblue

regression/goto-instrument/constant_propagator_unreachable/test.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+void unreachable(void)
+{
+  int x = 0;
+  assert(x != 0);
+}
+
+int main(void)
+{
+  return 0;
+}

regression/goto-instrument/constant_propagator_unreachable/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--constant-propagator
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+failed to find state
+--
+This is testing for a previous regression that caused constant propagation to
+fail in unreachable code

src/analyses/constant_propagator.cpp

@@ -751,8 +751,10 @@ void constant_propagator_ait::replace(
 {
   Forall_goto_program_instructions(it, goto_function.body)
   {
-    // Works because this is a location (but not history) sensitive domain
-    const constant_propagator_domaint &d = (*this)[it];
+    auto const current_domain_ptr =
+      std::dynamic_pointer_cast<const constant_propagator_domaint>(
+        this->abstract_state_before(it));
+    const constant_propagator_domaint &d = *current_domain_ptr;
 
     if(d.is_bottom())
       continue;