Write through a value-set-pointer

Tests determinate and indeterminate write through a pointer

Author: jezhiggins

regression/goto-analyzer/pointer-write-through-indeterminate/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main()
+{
+  int unknown;
+  int a = 10;
+  int b = 10;
+  int *p = &a;
+
+  if(unknown)
+  {
+    b = 15;
+    *p = 15;
+  }
+
+  assert(*p == b);
+}

regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-constants.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-values intervals --vsd-pointers constants
+^\[main.assertion.1\] line 16 assertion \*p == b: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-top-bottom.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-values intervals --vsd-pointers top-bottom
+^\[main.assertion.1\] line 16 assertion \*p == b: UNKNOWN
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-value-sets.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-values intervals --vsd-pointers value-set
+^\[main.assertion.1\] line 16 assertion \*p == b: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-write-through/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  int a = 10;
+  int *p = &a;
+
+  *p = 15;
+
+  assert(a == 15);
+}

regression/goto-analyzer/pointer-write-through/test-constants.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-pointers constants
+^\[main.assertion.1\] line 10 assertion a == 15: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-write-through/test-top-bottom.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-pointers top-bottom
+^\[main.assertion.1\] line 10 assertion a == 15: UNKNOWN
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-write-through/test-value-sets.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verify --variable-sensitivity --vsd-pointers value-set
+^\[main.assertion.1\] line 10 assertion a == 15: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--

src/analyses/variable-sensitivity/abstract_pointer_object.h

@@ -73,7 +73,6 @@ class abstract_pointer_objectt : public abstract_objectt,
     const abstract_environmentt &env,
     const namespacet &ns) const;
 
-protected:
   /// Evaluate writing to a pointer's value. More precise abstractions
   /// may override this provide more precise results.
   ///

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -115,6 +115,30 @@ abstract_object_pointert value_set_pointer_abstract_objectt::read_dereference(
   return results.first();
 }
 
+abstract_object_pointert value_set_pointer_abstract_objectt::write_dereference(
+  abstract_environmentt &environment,
+  const namespacet &ns,
+  const std::stack<exprt> &stack,
+  const abstract_object_pointert &new_value,
+  bool merging_write) const
+{
+  if(is_top() || is_bottom())
+  {
+    return abstract_pointer_objectt::write_dereference(
+      environment, ns, stack, new_value, merging_write);
+  }
+
+  for(auto value : values)
+  {
+    auto pointer =
+      std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
+    pointer->write_dereference(
+      environment, ns, stack, new_value, merging_write);
+  }
+
+  return shared_from_this();
+}
+
 abstract_object_pointert value_set_pointer_abstract_objectt::resolve_new_values(
   const abstract_object_sett &new_values,
   const abstract_environmentt &environment) const

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h

@@ -57,6 +57,13 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
     const abstract_environmentt &env,
     const namespacet &ns) const override;
 
+  abstract_object_pointert write_dereference(
+    abstract_environmentt &environment,
+    const namespacet &ns,
+    const std::stack<exprt> &stack,
+    const abstract_object_pointert &new_value,
+    bool merging_write) const override;
+
   void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
     const override;