@@ -17,6 +17,8 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]")
17
17
const std::size_t pointer_bits = 64 ;
18
18
SECTION (" Address of symbol" )
19
19
{
20
+ // Constructed address of expression should be equivalent to the following
21
+ // C expression - `&base`.
20
22
const typet base_type = unsignedbv_typet{8 };
21
23
const symbol_exprt object_base{" base" , base_type};
22
24
const address_of_exprt address_of{
@@ -26,6 +28,8 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]")
26
28
}
27
29
SECTION (" Address of index" )
28
30
{
31
+ // Constructed address of expression should be equivalent to the following
32
+ // C expression - `&(base[index])`.
29
33
const unsignedbv_typet element_type{8 };
30
34
const signedbv_typet index_type{pointer_bits};
31
35
const array_typet base_type{element_type, from_integer (42 , index_type)};
@@ -39,6 +43,8 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]")
39
43
}
40
44
SECTION (" Address of struct member" )
41
45
{
46
+ // Constructed address of expression should be equivalent to the following
47
+ // C expression - `&(base.baz)`.
42
48
const struct_tag_typet base_type{" structt" };
43
49
const symbol_exprt object_base{" base" , base_type};
44
50
const unsignedbv_typet member_type{8 };
@@ -50,6 +56,8 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]")
50
56
}
51
57
SECTION (" Address of index of struct member" )
52
58
{
59
+ // Constructed address of expression should be equivalent to the following
60
+ // C expression - `&(base.baz[index])`.
53
61
const struct_tag_typet base_type{" structt" };
54
62
const symbol_exprt object_base{" base" , base_type};
55
63
@@ -66,6 +74,8 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]")
66
74
}
67
75
SECTION (" Address of struct member at index" )
68
76
{
77
+ // Constructed address of expression should be equivalent to the following
78
+ // C expression - `&(base[index].qux)`.
69
79
const struct_tag_typet element_type{" struct_elementt" };
70
80
const signedbv_typet index_type{pointer_bits};
71
81
const array_typet base_type{element_type, from_integer (42 , index_type)};
0 commit comments