Vsd value set of pointers

regression/goto-analyzer/pointer-dereference-indeterminate-values/main.c

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

regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-constants.desc

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

regression/goto-analyzer/pointer-dereference-indeterminate-values/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 15 assertion q == a: UNKNOWN
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-dereference-indeterminate-values/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 15 assertion q == a: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-analyzer/pointer-dereference/main.c

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

regression/goto-analyzer/pointer-dereference/test-constants.desc

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

regression/goto-analyzer/pointer-dereference/test-top-bottom.desc

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

regression/goto-analyzer/pointer-dereference/test-value-sets.desc

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

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$
+--

scripts/expected_doxygen_warnings.txt

@@ -97,6 +97,6 @@ warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (1
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (245), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_types.h' not generated, too many nodes (122), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (244), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_types.h' not generated, too many nodes (121), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/Makefile

@@ -33,29 +33,29 @@ SRC = ai.cpp \
       static_analysis.cpp \
       uncaught_exceptions_analysis.cpp \
       uninitialized_domain.cpp \
-      variable-sensitivity/abstract_object.cpp \
       variable-sensitivity/abstract_environment.cpp \
+      variable-sensitivity/abstract_object.cpp \
+      variable-sensitivity/abstract_object_set.cpp \
+      variable-sensitivity/abstract_pointer_object.cpp \
       variable-sensitivity/abstract_value_object.cpp \
       variable-sensitivity/constant_abstract_value.cpp \
       variable-sensitivity/constant_pointer_abstract_object.cpp \
       variable-sensitivity/context_abstract_object.cpp \
-      variable-sensitivity/write_location_context.cpp \
-      variable-sensitivity/pointer_abstract_object.cpp \
-      variable-sensitivity/variable_sensitivity_domain.cpp \
-      variable-sensitivity/variable_sensitivity_object_factory.cpp \
-      variable-sensitivity/full_struct_abstract_object.cpp \
-      variable-sensitivity/full_array_abstract_object.cpp \
-      variable-sensitivity/write_stack.cpp \
-      variable-sensitivity/write_stack_entry.cpp \
       variable-sensitivity/data_dependency_context.cpp \
-      variable-sensitivity/value_set_abstract_object.cpp \
-      variable-sensitivity/variable_sensitivity_dependence_graph.cpp \
+      variable-sensitivity/full_array_abstract_object.cpp \
+      variable-sensitivity/full_struct_abstract_object.cpp \
       variable-sensitivity/interval_abstract_value.cpp \
+      variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
       variable-sensitivity/value_set_abstract_object.cpp \
       variable-sensitivity/value_set_abstract_value.cpp \
       variable-sensitivity/value_set_pointer_abstract_object.cpp \
-      variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
       variable-sensitivity/variable_sensitivity_configuration.cpp \
+      variable-sensitivity/variable_sensitivity_dependence_graph.cpp \
+      variable-sensitivity/variable_sensitivity_domain.cpp \
+      variable-sensitivity/variable_sensitivity_object_factory.cpp \
+      variable-sensitivity/write_location_context.cpp \
+      variable-sensitivity/write_stack.cpp \
+      variable-sensitivity/write_stack_entry.cpp \
       # Empty last line
 
 INCLUDES= -I ..

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -11,8 +11,8 @@
 #include <analyses/variable-sensitivity/abstract_object.h>
 #include <analyses/variable-sensitivity/abstract_object_statistics.h>
 #include <analyses/variable-sensitivity/constant_abstract_value.h>
-#include <analyses/variable-sensitivity/pointer_abstract_object.h>
 #include <analyses/variable-sensitivity/two_value_array_abstract_object.h>
+#include <analyses/variable-sensitivity/two_value_pointer_abstract_object.h>
 #include <analyses/variable-sensitivity/two_value_struct_abstract_object.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
 #include <util/pointer_expr.h>

src/analyses/variable-sensitivity/abstract_object_set.cpp

@@ -0,0 +1,36 @@
+/*******************************************************************\
+
+ Module: analyses variable-sensitivity
+
+ Author: Jez Higgins, [email protected]
+
+\*******************************************************************/
+
+#include <analyses/variable-sensitivity/abstract_object_set.h>
+#include <util/string_utils.h>
+
+static bool by_length(const std::string &lhs, const std::string &rhs)
+{
+  if(lhs.size() < rhs.size())
+    return true;
+  if(lhs.size() > rhs.size())
+    return false;
+  return lhs < rhs;
+}
+
+void abstract_object_sett::output(
+  std::ostream &out,
+  const ai_baset &ai,
+  const namespacet &ns) const
+{
+  std::vector<std::string> output_values;
+  for(const auto &value : values)
+  {
+    std::ostringstream ss;
+    value->output(ss, ai, ns);
+    output_values.emplace_back(ss.str());
+  }
+  std::sort(output_values.begin(), output_values.end(), by_length);
+
+  join_strings(out, output_values.begin(), output_values.end(), ", ");
+}

src/analyses/variable-sensitivity/abstract_object_set.h

@@ -0,0 +1,83 @@
+/*******************************************************************\
+
+ Module: analyses variable-sensitivity
+
+ Author: Jez Higgins, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// an unordered set of value objects
+
+#ifndef CBMC_ABSTRACT_OBJECT_SET_H
+#define CBMC_ABSTRACT_OBJECT_SET_H
+
+#include <analyses/variable-sensitivity/abstract_value_object.h>
+#include <unordered_set>
+
+class abstract_object_sett
+{
+public:
+  using value_sett = std::unordered_set<
+    abstract_object_pointert,
+    abstract_hashert,
+    abstract_equalert>;
+  using const_iterator = value_sett::const_iterator;
+  using value_type = value_sett::value_type;
+  using size_type = value_sett::size_type;
+
+  void insert(const abstract_object_pointert &o)
+  {
+    values.insert(o);
+  }
+  void insert(abstract_object_pointert &&o)
+  {
+    values.insert(std::move(o));
+  }
+  void insert(const abstract_object_sett &rhs)
+  {
+    values.insert(rhs.begin(), rhs.end());
+  }
+
+  abstract_object_pointert first() const
+  {
+    return *begin();
+  }
+
+  const_iterator begin() const
+  {
+    return values.begin();
+  }
+  const_iterator end() const
+  {
+    return values.end();
+  }
+
+  value_sett::size_type size() const
+  {
+    return values.size();
+  }
+  bool empty() const
+  {
+    return values.empty();
+  }
+
+  bool operator==(const abstract_object_sett &rhs) const
+  {
+    return values == rhs.values;
+  }
+
+  void
+  output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const;
+
+private:
+  value_sett values;
+};
+
+class value_set_tag
+{
+public:
+  virtual const abstract_object_sett &get_values() const = 0;
+};
+
+#endif //CBMC_ABSTRACT_OBJECT_SET_H