Merge pull request diffblue#430 from diffblue/bugfix_taint_no_fresh_EVS_for_DO_query

Bugfix in taint analysis: Do not create fresh EVS when the query is DO.

Author: marek-trtik

src/taint-analysis/taint_summary.cpp

@@ -431,17 +431,22 @@ bool taint_algorithm_computing_summary_of_functiont::
     singular);
   if(generate_fresh_evs && raw_result.empty())
   {
-    external_value_set_exprt new_lhs(
-      query_expr.type(),
-      constant_exprt("", string_typet()),
-      external_value_set_typet::ROOT_OBJECT,
-      false);
-    // Use access path "[]" to dereference the pointer
-    access_path_entry_exprt new_entry("[]", "", "", typet());
-    new_lhs.set_per_field_access_path(new_entry);
-    const auto new_number =
-      numbering->number(static_cast<const exprt &>(new_lhs));
-    result.insert(new_number);
+    if(query_expr.id() == ID_dynamic_object)
+      result.insert(numbering->number(query_expr));
+    else
+    {
+      external_value_set_exprt new_lhs(
+        query_expr.type(),
+        constant_exprt("", string_typet()),
+        external_value_set_typet::ROOT_OBJECT,
+        false);
+      // Use access path "[]" to dereference the pointer
+      access_path_entry_exprt new_entry("[]", "", "", typet());
+      new_lhs.set_per_field_access_path(new_entry);
+      const auto new_number =
+        numbering->number(static_cast<const exprt &>(new_lhs));
+      result.insert(new_number);
+    }
     return false;
   }
   for(const auto raw_number : raw_result)