Bugfix: Explicit retrievals of DOs from value_set amd reaching_defs.

Author: marek-trtik

src/analyses/goto_rw.cpp

@@ -613,6 +613,17 @@ void rw_range_set_value_sett::get_objects_dereference(
     new_size=std::min(size, new_size);
   }
 
+  if(object.is_not_nil() && object.id()==ID_symbol &&
+    as_string(to_symbol_expr(object).get_identifier()).find(
+      get_vsderef_dynamic_object_prefix())==0UL)
+  {
+    add(
+      mode,
+      to_symbol_expr(object).get_identifier(),
+      range_start,
+      range_start + new_size);
+  }
+
   // value_set_dereferencet::build_reference_to will turn *p into
   // DYNAMIC_OBJECT(p) ? *p : invalid_objectN
   if(object.is_not_nil() &&

src/analyses/reaching_definitions.cpp

@@ -22,6 +22,7 @@ Date: February 2013
 #include <util/make_unique.h>
 
 #include <pointer-analysis/value_set_analysis_fi.h>
+#include <pointer-analysis/value_set_dereference.h>
 
 #include "is_threaded.h"
 #include "dirty.h"
@@ -309,21 +310,25 @@ void rd_range_domaint::transform_assign(
   forall_rw_range_set_w_objects(it, rw_set)
   {
     const irep_idt &identifier=it->first;
-    // ignore symex::invalid_object
+    bool do_kill=is_must_alias;
     const symbolt *symbol_ptr;
     if(ns.lookup(identifier, symbol_ptr))
-      continue;
-    INVARIANT_STRUCTURED(
-      symbol_ptr!=nullptr,
-      nullptr_exceptiont,
-      "Symbol is in symbol table");
+    {
+      if(as_string(identifier).find(get_vsderef_dynamic_object_prefix())!=0UL)
+        // ignore symex::invalid_object
+        continue;
+    }
+    else
+    {
+      do_kill = do_kill &&
+       (!rd.get_is_threaded()(from) ||
+        (!symbol_ptr->is_shared() &&
+         !rd.get_is_dirty()(identifier)));
+    }
 
     const range_domaint &ranges=rw_set.get_ranges(it);
 
-    if(is_must_alias &&
-       (!rd.get_is_threaded()(from) ||
-        (!symbol_ptr->is_shared() &&
-         !rd.get_is_dirty()(identifier))))
+    if(do_kill)
       for(const auto &range : ranges)
         kill(identifier, range.first, range.second);
 

src/pointer-analysis/value_set_dereference.cpp

@@ -60,6 +60,12 @@ const exprt &value_set_dereferencet::get_symbol(const exprt &expr)
   return expr;
 }
 
+const std::string &get_vsderef_dynamic_object_prefix()
+{
+  static std::string prefix(CPROVER_PREFIX "_VSDEREF_");
+  return prefix;
+}
+
 /// \par parameters: expression dest, to be dereferenced under given guard,
 /// and given mode
 /// \return returns pointer after dereferencing
@@ -344,7 +350,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     result.pointer_guard=dynamic_object_expr;
 
     // can't remove here, turn into *p
-    result.value=dereference_exprt(pointer_expr, dereference_type);
+    result.value=symbol_exprt(
+      get_vsderef_dynamic_object_prefix() + from_expr(root_object),
+      ns.follow(dereference_type));
 
     if(options.get_bool_option("pointer-check"))
     {

src/pointer-analysis/value_set_dereference.h

@@ -144,4 +144,6 @@ class value_set_dereferencet
     const exprt &offset);
 };
 
+const std::string &get_vsderef_dynamic_object_prefix();
+
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H