Create cpp file for array_element_from_pointer

This is so that the function can be used in more than just one place.

Author: antlechner

src/util/Makefile

@@ -1,5 +1,6 @@
 SRC = allocate_objects.cpp \
       arith_tools.cpp \
+      array_element_from_pointer.cpp \
       array_name.cpp \
       base_type.cpp \
       bv_arithmetic.cpp \

src/util/array_element_from_pointer.cpp

@@ -0,0 +1,18 @@
+/*******************************************************************\
+
+Module: Element access in a pointer array
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include "array_element_from_pointer.h"
+
+dereference_exprt
+array_element_from_pointer(const exprt &pointer, const exprt &index)
+{
+  PRECONDITION(can_cast_type<pointer_typet>(pointer.type()));
+  PRECONDITION(
+    index.type().id() == ID_signedbv || index.type().id() == ID_unsignedbv);
+  return dereference_exprt{plus_exprt{pointer, index}};
+}

src/util/array_element_from_pointer.h

@@ -22,12 +22,6 @@ Author: Diffblue Ltd.
 /// \param index: index of the element to access
 /// \return expression representing the (\p index)'th element of the array
 dereference_exprt
-array_element_from_pointer(const exprt &pointer, const exprt &index)
-{
-  PRECONDITION(can_cast_type<pointer_typet>(pointer.type()));
-  PRECONDITION(
-    index.type().id() == ID_signedbv || index.type().id() == ID_unsignedbv);
-  return dereference_exprt{plus_exprt{pointer, index}};
-}
+array_element_from_pointer(const exprt &pointer, const exprt &index);
 
 #endif // CPROVER_UTIL_ARRAY_ELEMENT_FROM_POINTER_H