Post-dominators: support multiple exit points

Programs with assume(false) or (unconditional) self loops include
instructions from which the regular program exit cannot be reached.
Nevertheless, such instructions still need to be included in
post-dominator computation.

Not doing so would result in missing control dependencies when building
the dependence graph, and thus in wrong slicing results (which the
included regression test previously showed).

Author: tautschnig

regression/goto-instrument/slice25/main.c

@@ -0,0 +1,13 @@
+int main()
+{
+#ifdef __GNUC__
+  int x = 1;
+  if(x == 0)
+  {
+    __CPROVER_assert(0, "");
+    // __builtin_types_compatible_p yields a proper "bool" typed constant
+    __CPROVER_assume(__builtin_types_compatible_p(double, float));
+  }
+#endif
+  return 0;
+}

regression/goto-instrument/slice25/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

src/analyses/cfg_dominators.h

@@ -163,6 +163,27 @@ void cfg_dominators_templatet<P, T, post_dom>::fixedpoint(P &program)
       ++s_it)
     worklist.push_back(cfg[s_it->first].PC);
 
+  // A program may have multiple "exit" nodes when self loops or assume(false)
+  // instructions are present.
+  if(post_dom)
+  {
+    for(auto &cfg_entry : cfg.entry_map)
+    {
+      if(cfg[cfg_entry.second].PC == entry_node)
+        continue;
+
+      typename cfgt::nodet &n_it = cfg[cfg_entry.second];
+      if(
+        n_it.out.empty() ||
+        (n_it.out.size() == 1 && n_it.out.begin()->first == cfg_entry.second))
+      {
+        n_it.dominators.insert(cfg[cfg_entry.second].PC);
+        for(const auto &predecessor : n_it.in)
+          worklist.push_back(cfg[predecessor.first].PC);
+      }
+    }
+  }
+
   while(!worklist.empty())
   {
     // get node from worklist