Merge pull request diffblue#255 from diffblue/issue206

Avoid breaking fixpoint when merging data_dependency_context

Author: chrisr-diffblue

regression/goto-analyzer/variable-sensitivity-dependence-graph-merge/main.c

@@ -0,0 +1,21 @@
+void cal(void)
+{
+
+}
+
+const int g_N = 5;
+int x = 0;
+
+struct {
+   int idx;
+} s_str = { 0 };
+
+void main(void)
+{
+  for (int i = 0; i < g_N; i++) {
+    cal();
+    s_str.idx = s_str.idx + 1;
+  }
+
+  __CPROVER_assert(s_str.idx > 1, "s_str.idx > 1");
+}

regression/goto-analyzer/variable-sensitivity-dependence-graph-merge/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--dependence-graph-vs --structs --arrays --verify
+EXIT=0
+SIGNAL=0
+^\[main.assertion.1\] file .* function main, idx==1: Unknown$
+--

src/analyses/variable-sensitivity/data_dependency_context.cpp

@@ -228,7 +228,13 @@ abstract_object_pointert data_dependency_contextt::merge(
       std::inserter(result->data_dominators, result->data_dominators.end()),
       location_ordert());
 
-    return result;
+    // It is critically important that we only return a newly constructed result
+    // abstract object *iff* the data has actually changed, otherwise AI may
+    // never reach a fixpoint
+    if(has_been_modified(result))
+      return result;
+    else
+      return shared_from_this();
   }
 
   return abstract_objectt::merge(other);