Add unit test for interpreter evaluation

Author: Matthias Güdemann

src/goto-programs/interpreter_class.h

@@ -306,6 +306,14 @@ class interpretert:public messaget
 
   void initialize(bool init);
   void show_state();
+
+  friend mp_vectort
+  interpreter_evaluate(interpretert &interpreter, const exprt &expr)
+  {
+    mp_vectort mp_vector;
+    interpreter.evaluate(expr, mp_vector);
+    return mp_vector;
+  }
 };
 
 #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 \
+       interpretert/interpreter.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I.

unit/interpreter/interpreter.cpp

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+ 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/namespace.h>
+
+SCENARIO("interpreter evaluation")
+{
+  symbol_tablet symbol_table;
+  goto_functionst goto_functions;
+  null_message_handlert null_message_handler;
+
+  interpretert interpreter(symbol_table, goto_functions, null_message_handler);
+
+  unsignedbv_typet java_char(16);
+  pointer_typet pointer_type(java_char, 64);
+
+  constant_exprt constant_expr(0, pointer_type);
+  interpretert::mp_vectort mp_vector =
+    interpreter_evaluate(interpreter, constant_expr);
+
+  REQUIRE(mp_vector.size() == 1);
+  REQUIRE(mp_vector[0].is_zero());
+}

unit/interpreter/module_dependencies.txt

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