Pull array helpers out of full_array merge unit tests

Author: jezhiggins

unit/Makefile

@@ -28,6 +28,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/variable-sensitivity/interval_abstract_value/merge.cpp \
        analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp \
        analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp \
+       analyses/variable-sensitivity/full_struct_abstract_object/array_builder.cpp \
        analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \
        analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp \
        analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp \

unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp

@@ -0,0 +1,63 @@
+/*******************************************************************\
+
+ Module: Unit tests helpers for arrays
+
+ Author: Jez Higgins, [email protected]
+
+\*******************************************************************/
+
+#include <analyses/variable-sensitivity/abstract_environment.h>
+#include <analyses/variable-sensitivity/full_array_abstract_object.h>
+#include <analyses/variable-sensitivity/full_array_abstract_object/array_builder.h>
+#include <arith_tools.h>
+#include <util/mathematical_types.h>
+
+full_array_abstract_objectt::full_array_pointert build_array(
+  const exprt &array_expr,
+  abstract_environmentt &environment,
+  const namespacet &ns)
+{
+  return std::make_shared<full_array_abstract_objectt>(
+    array_expr, environment, ns);
+}
+
+full_array_abstract_objectt::full_array_pointert build_array(
+  const std::vector<int> &array,
+  abstract_environmentt &environment,
+  const namespacet &ns)
+{
+  const array_typet array_type(
+    integer_typet(), from_integer(array.size(), integer_typet()));
+
+  exprt::operandst element_ops;
+
+  for(auto element : array)
+    element_ops.push_back(from_integer(element, integer_typet()));
+
+  auto array_expr = array_exprt(element_ops, array_type);
+  return build_array(array_expr, environment, ns);
+}
+
+full_array_abstract_objectt::full_array_pointert build_top_array()
+{
+  auto array_type =
+    array_typet(integer_typet(), from_integer(3, integer_typet()));
+  return std::make_shared<full_array_abstract_objectt>(array_type, true, false);
+}
+
+full_array_abstract_objectt::full_array_pointert build_bottom_array()
+{
+  auto array_type =
+    array_typet(integer_typet(), from_integer(3, integer_typet()));
+  return std::make_shared<full_array_abstract_objectt>(array_type, false, true);
+}
+
+exprt read_index(
+  full_array_abstract_objectt::full_array_pointert array_object,
+  const index_exprt &index,
+  abstract_environmentt &environment,
+  const namespacet &ns)
+{
+  return array_object->expression_transform(index, {}, environment, ns)
+    ->to_constant();
+}

unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+ Module: Unit tests helpers for arrays
+
+ Author: Jez Higgins, [email protected]
+
+\*******************************************************************/
+#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_ARRAY_BUILDER_H
+#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_ARRAY_BUILDER_H
+
+#include <analyses/variable-sensitivity/full_array_abstract_object.h>
+
+full_array_abstract_objectt::full_array_pointert build_array(
+  const exprt &array_expr,
+  abstract_environmentt &environment,
+  const namespacet &ns);
+
+full_array_abstract_objectt::full_array_pointert build_array(
+  const std::vector<int> &array,
+  abstract_environmentt &environment,
+  const namespacet &ns);
+
+full_array_abstract_objectt::full_array_pointert build_top_array();
+
+full_array_abstract_objectt::full_array_pointert build_bottom_array();
+
+exprt read_index(
+  full_array_abstract_objectt::full_array_pointert array_object,
+  const index_exprt &index,
+  abstract_environmentt &environment,
+  const namespacet &ns);
+
+#endif