constant pointer to_predicate

Author: jezhiggins

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -388,3 +388,9 @@ exprt constant_pointer_abstract_objectt::ptr_comparison_expr(
     return true_exprt();
   return nil_exprt();
 }
+
+exprt constant_pointer_abstract_objectt::to_predicate_internal(
+  const exprt &name) const
+{
+  return equal_exprt(name, value_stack.to_expression());
+}

src/analyses/variable-sensitivity/constant_pointer_abstract_object.h

@@ -145,6 +145,8 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt
 
   CLONE
 
+  exprt to_predicate_internal(const exprt &name) const override;
+
 private:
   bool same_target(abstract_object_pointert other) const;
   exprt offset() const;

unit/Makefile

@@ -20,6 +20,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/variable-sensitivity/constant_abstract_value/meet.cpp \
        analyses/variable-sensitivity/constant_abstract_value/merge.cpp \
        analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp \
+       analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp \
        analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp \
        analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \
        analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp \

unit/analyses/variable-sensitivity/constant_pointer_abstract_object/module_dependencies.txt

@@ -0,0 +1,3 @@
+analyses
+testing-utils
+util

unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp

@@ -0,0 +1,59 @@
+/*******************************************************************\
+
+ Module: Tests for constant_pointer_abstract_objectt::to_predicate
+
+ Author: Jez Higgins
+
+\*******************************************************************/
+
+#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
+#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
+#include <testing-utils/use_catch.h>
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/pointer_expr.h>
+
+SCENARIO(
+  "constant_pointer_abstract_object to predicate",
+  "[core][analyses][variable-sensitivity][constant_pointer_abstract_object][to_"
+  "predicate]")
+{
+  const auto int_type = signedbv_typet(32);
+  const auto ptr_type = pointer_typet(int_type, 32);
+  const auto val2_symbol = symbol_exprt(dstringt("val2"), int_type);
+
+  const auto x_name = symbol_exprt(dstringt("x"), int_type);
+
+  auto config = vsd_configt::constant_domain();
+  config.context_tracking.data_dependency_context = false;
+  config.context_tracking.last_write_context = false;
+  auto object_factory =
+    variable_sensitivity_object_factoryt::configured_with(config);
+  abstract_environmentt environment{object_factory};
+  environment.make_top();
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  GIVEN("constant_pointer_abstract_object")
+  {
+    WHEN("it is TOP")
+    {
+      auto obj = std::make_shared<constant_pointer_abstract_objectt>(
+        ptr_type, true, false);
+      THEN_PREDICATE(obj, "TRUE");
+    }
+    WHEN("it is BOTTOM")
+    {
+      auto obj = std::make_shared<constant_pointer_abstract_objectt>(
+        ptr_type, false, true);
+      THEN_PREDICATE(obj, "FALSE");
+    }
+    WHEN("points to a &symbol")
+    {
+      const auto address_of = address_of_exprt(val2_symbol);
+      auto obj = std::make_shared<constant_pointer_abstract_objectt>(
+        address_of, environment, ns);
+      THEN_PREDICATE(obj, "x == &val2");
+    }
+  }
+}