Cleanup value_set_dereferencet's internal API

Several parameters were no longer used and thus unnecessarily being passed
around.

Author: tautschnig

src/pointer-analysis/value_set_dereference.cpp

@@ -101,7 +101,7 @@ exprt value_set_dereferencet::dereference(
       it!=points_to_set.end();
       it++)
   {
-    valuet value=build_reference_to(*it, mode, pointer, guard);
+    valuet value = build_reference_to(*it, pointer);
 
     #if 0
     std::cout << "V: " << format(value.pointer_guard) << " --> ";
@@ -270,9 +270,7 @@ bool value_set_dereferencet::dereference_type_compare(
 
 value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
   const exprt &what,
-  const modet mode,
-  const exprt &pointer_expr,
-  const guardt &guard)
+  const exprt &pointer_expr)
 {
   const typet &dereference_type=
     ns.follow(pointer_expr.type()).subtype();
@@ -397,9 +395,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       result.pointer_guard=same_object(pointer_expr, object_pointer);
     }
 
-    guardt tmp_guard(guard);
-    tmp_guard.add(result.pointer_guard);
-
     const typet &object_type=ns.follow(object.type());
     const exprt &root_object=o.root_object();
     const typet &root_object_type=ns.follow(root_object.type());
@@ -492,7 +487,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       else
         offset=o.offset();
 
-      if(memory_model(result.value, dereference_type, tmp_guard, offset))
+      if(memory_model(result.value, dereference_type, offset))
       {
         // ok, done
       }
@@ -519,7 +514,6 @@ static bool is_a_bv_type(const typet &type)
 bool value_set_dereferencet::memory_model(
   exprt &value,
   const typet &to_type,
-  const guardt &guard,
   const exprt &offset)
 {
   // we will allow more or less arbitrary pointer type cast
@@ -543,7 +537,7 @@ bool value_set_dereferencet::memory_model(
       {
       }
       else
-        return memory_model_conversion(value, to_type, guard, offset);
+        return memory_model_conversion(value, to_type);
     }
   }
 
@@ -553,19 +547,17 @@ bool value_set_dereferencet::memory_model(
      to_type.id()==ID_pointer)
   {
     if(pointer_offset_bits(from_type, ns) == pointer_offset_bits(to_type, ns))
-      return memory_model_conversion(value, to_type, guard, offset);
+      return memory_model_conversion(value, to_type);
   }
 
   // otherwise, we will stitch it together from bytes
 
-  return memory_model_bytes(value, to_type, guard, offset);
+  return memory_model_bytes(value, to_type, offset);
 }
 
 bool value_set_dereferencet::memory_model_conversion(
   exprt &value,
-  const typet &to_type,
-  const guardt &guard,
-  const exprt &offset)
+  const typet &to_type)
 {
   // only doing type conversion
   // just do the typecast
@@ -576,7 +568,6 @@ bool value_set_dereferencet::memory_model_conversion(
 bool value_set_dereferencet::memory_model_bytes(
   exprt &value,
   const typet &to_type,
-  const guardt &guard,
   const exprt &offset)
 {
   const typet from_type=value.type();

src/pointer-analysis/value_set_dereference.h

@@ -113,10 +113,7 @@ class value_set_dereferencet
   /// \param what: value set entry to convert to an expression: either
   ///   ID_unknown, ID_invalid, or an object_descriptor_exprt giving a referred
   ///   object and offset.
-  /// \param mode: whether the pointer is being read or written; used to create
-  ///   pointer validity checks if need be
   /// \param pointer: pointer expression that may point to `what`
-  /// \param guard: guard under which the pointer is dereferenced
   /// \return
   ///    * If we were explicitly instructed to ignore `what` as a possible
   ///        pointer target: a `valuet` with `ignore` = true, and `value` and
@@ -128,11 +125,7 @@ class value_set_dereferencet
   ///        `{.value = global, .pointer_guard = (pointer_expr == &global)}`
   ///    * Otherwise, if we couldn't build an expression (e.g. for `what` ==
   ///        ID_unknown), a `valuet` with nil `value` and `ignore` == false.
-  valuet build_reference_to(
-    const exprt &what,
-    const modet mode,
-    const exprt &pointer,
-    const guardt &guard);
+  valuet build_reference_to(const exprt &what, const exprt &pointer);
 
   bool get_value_guard(
     const exprt &symbol,
@@ -141,22 +134,13 @@ class value_set_dereferencet
 
   static const exprt &get_symbol(const exprt &object);
 
-  bool memory_model(
-    exprt &value,
-    const typet &type,
-    const guardt &guard,
-    const exprt &offset);
+  bool memory_model(exprt &value, const typet &type, const exprt &offset);
 
-  bool memory_model_conversion(
-    exprt &value,
-    const typet &type,
-    const guardt &guard,
-    const exprt &offset);
+  bool memory_model_conversion(exprt &value, const typet &type);
 
   bool memory_model_bytes(
     exprt &value,
     const typet &type,
-    const guardt &guard,
     const exprt &offset);
 };