Only apply field_sensitivity to dereferenced object

This is important to consider dereferenced object as read value.

Author: romainbrenguier

src/goto-symex/symex_dereference.cpp

@@ -369,6 +369,20 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
   }
 }
 
+static exprt apply_to_objects_in_dereference(
+  exprt e, const std::function<exprt(exprt)> &f)
+{
+  if(auto deref = expr_try_dynamic_cast<dereference_exprt>(e))
+  {
+    deref->op() = f(std::move(deref->op()));
+    return *deref;
+  }
+
+  for(auto &sub : e.operands())
+    sub = apply_to_objects_in_dereference(std::move(sub), f);
+  return e;
+}
+
 /// Replace all dereference operations within \p expr with explicit references
 /// to the objects they may refer to. For example, the expression `*p1 + *p2`
 /// might be rewritten to `obj1 + (p2 == &obj2 ? obj2 : obj3)` in the case where
@@ -408,19 +422,20 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
 ///    See \ref auto_objects.cpp for details.
 void goto_symext::dereference(exprt &expr, statet &state, bool write)
 {
-  // The expression needs to be renamed to level 1
-  // in order to distinguish addresses of local variables
-  // from different frames. Would be enough to rename
-  // symbols whose address is taken.
   PRECONDITION(!state.call_stack().empty());
-  exprt l1_expr = state.field_sensitivity.apply(
-    ns, state, state.rename<L1>(expr, ns).get(), write);
+
+  // Symbols whose address is taken need to be renamed to level 1
+  // in order to distinguish addresses of local variables
+  // from different frames.
+  expr = apply_to_objects_in_dereference(std::move(expr), [&](exprt e) {
+      return state.field_sensitivity.apply(
+        ns, state, state.rename<L1>(std::move(e), ns).get(), false);});
 
   // start the recursion!
-  dereference_rec(l1_expr, state, write);
+  dereference_rec(expr, state, write);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
-  expr = state.rename<L1>(std::move(l1_expr), ns).get();
+  expr = state.rename<L1>(std::move(expr), ns).get();
 
   // Dereferencing is likely to introduce new member-of-if constructs --
   // for example, "x->field" may have become "(x == &o1 ? o1 : o2).field."