Add unit test for interpreter evaluation

Author: Matthias Güdemann

src/goto-programs/interpreter_class.h

@@ -306,6 +306,8 @@ class interpretert:public messaget
 
   void initialize(bool init);
   void show_state();
+
+  friend class interpreter_testt;
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H

unit/Makefile

@@ -45,6 +45,7 @@ SRC += unit_tests.cpp \
        util/symbol_table.cpp \
        util/unicode.cpp \
        catch_example.cpp \
+       interpreter/interpreter.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I.

unit/interpreter/interpreter.cpp

@@ -0,0 +1,72 @@
+/*******************************************************************\
+
+ Module: Interpreter unit tests.
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+#include <goto-programs/goto_functions.h>
+#include <goto-programs/interpreter_class.h>
+#include <util/message.h>
+#include <util/mp_arith.h>
+#include <util/namespace.h>
+
+typedef interpretert::mp_vectort mp_vectort;
+
+class interpreter_testt
+{
+  symbol_tablet symbol_table;
+  goto_functionst goto_functions;
+  null_message_handlert null_message_handler;
+  interpretert interpreter;
+
+public:
+  explicit interpreter_testt()
+    : interpreter(symbol_table, goto_functions, null_message_handler)
+  {
+  }
+
+  mp_vectort evaluate(const exprt &expression)
+  {
+    mp_vectort result;
+    interpreter.evaluate(expression, result);
+    return result;
+  }
+};
+
+SCENARIO("interpreter evaluation null pointer expressions")
+{
+  interpreter_testt interpreter_test;
+  mp_vectort null_vector = {0};
+
+  THEN("null pointer without operands")
+  {
+    unsignedbv_typet java_char(16);
+    pointer_typet pointer_type(java_char, 64);
+
+    constant_exprt constant_expr(ID_NULL, pointer_type);
+
+    mp_vectort mp_vector = interpreter_test.evaluate(constant_expr);
+
+    REQUIRE_THAT(mp_vector, Catch::Equals(null_vector));
+  }
+  THEN("null pointer with operands")
+  {
+    pointer_typet outer_pointer_type(empty_typet(), 64);
+    constant_exprt outer_expression(
+      "0000000000000000000000000000000000000000000000000000000000000000",
+      outer_pointer_type);
+
+    pointer_typet inner_pointer_type(empty_typet(), 64);
+    constant_exprt inner_expression(ID_NULL, inner_pointer_type);
+
+    outer_expression.move_to_operands(inner_expression);
+
+    mp_vectort mp_vector = interpreter_test.evaluate(outer_expression);
+
+    REQUIRE_THAT(mp_vector, Catch::Equals(null_vector));
+  }
+}

unit/interpreter/module_dependencies.txt

@@ -0,0 +1,3 @@
+goto-programs
+testing-utils
+util