1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
/*******************************************************************\
Module: Interpreter unit tests.
Author: Diffblue Ltd.
\*******************************************************************/
#include <goto-programs/interpreter_class.h>
#include <util/message.h>
#include <util/mp_arith.h>
#include <util/pointer_expr.h>
#include <util/symbol_table.h>
#include <goto-programs/goto_functions.h>
#include <testing-utils/use_catch.h>
#include <climits>
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)
{
return interpreter.evaluate(expression);
}
};
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, sizeof(void *) * CHAR_BIT);
null_pointer_exprt constant_expr{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(), sizeof(void *) * CHAR_BIT);
constant_exprt outer_expression(
"0000000000000000000000000000000000000000000000000000000000000000",
outer_pointer_type);
outer_expression.add_to_operands(null_pointer_exprt(
pointer_typet(empty_typet(), sizeof(void *) * CHAR_BIT)));
mp_vectort mp_vector = interpreter_test.evaluate(outer_expression);
REQUIRE_THAT(mp_vector, Catch::Equals(null_vector));
}
}
|
