Skip to content

Commit 4524b08

Browse files
author
Matthias Güdemann
committed
Add unit test for interpreter evaluation
1 parent 55a1dfe commit 4524b08

File tree

2 files changed

+41
-0
lines changed

2 files changed

+41
-0
lines changed

src/goto-programs/interpreter_class.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -306,6 +306,14 @@ class interpretert:public messaget
306306

307307
void initialize(bool init);
308308
void show_state();
309+
310+
friend mp_vectort
311+
interpreter_evaluate(interpretert &interpreter, const exprt &expr)
312+
{
313+
mp_vectort mp_vector;
314+
interpreter.evaluate(expr, mp_vector);
315+
return mp_vector;
316+
}
309317
};
310318

311319
#endif // CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H

unit/interpreter/interpreter.cpp

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
/*******************************************************************\
2+
3+
Module: Interpreter unit tests.
4+
5+
Author: Diffblue Ltd.
6+
7+
\*******************************************************************/
8+
9+
#include <testing-utils/catch.hpp>
10+
11+
#include <goto-programs/goto_functions.h>
12+
#include <goto-programs/interpreter_class.h>
13+
#include <util/message.h>
14+
#include <util/namespace.h>
15+
16+
SCENARIO("interpreter evaluation")
17+
{
18+
symbol_tablet symbol_table;
19+
goto_functionst goto_functions;
20+
null_message_handlert null_message_handler;
21+
22+
interpretert interpreter(symbol_table, goto_functions, null_message_handler);
23+
24+
unsignedbv_typet java_char(16);
25+
pointer_typet pointer_type(java_char, 64);
26+
27+
constant_exprt constant_expr(0, pointer_type);
28+
interpretert::mp_vectort mp_vector =
29+
interpreter_evaluate(interpreter, constant_expr);
30+
31+
REQUIRE(mp_vector.size() == 1);
32+
REQUIRE(mp_vector[0].is_zero());
33+
}

0 commit comments

Comments
 (0)