@@ -32,7 +32,7 @@ TEST_CASE(
32
32
REQUIRE (test.struct_encoding .encode (input) == input);
33
33
}
34
34
35
- TEST_CASE (" struct encoding of struct_tag_type " , " [core][smt2_incremental]" )
35
+ TEST_CASE (" struct encoding of types " , " [core][smt2_incremental]" )
36
36
{
37
37
const struct_union_typet::componentst components{
38
38
{" foo" , unsignedbv_typet{8 }}, {" bar" , signedbv_typet{16 }}};
@@ -41,45 +41,30 @@ TEST_CASE("struct encoding of struct_tag_type", "[core][smt2_incremental]")
41
41
auto test = struct_encoding_test_environmentt::make ();
42
42
test.symbol_table .insert (type_symbol);
43
43
struct_tag_typet struct_tag{type_symbol.name };
44
- REQUIRE (test.struct_encoding .encode (struct_tag) == bv_typet{24 });
45
- }
46
-
47
- TEST_CASE (" struct encoding of array of structs" , " [core][smt2_incremental]" )
48
- {
49
- const struct_union_typet::componentst components{
50
- {" foo" , unsignedbv_typet{8 }}, {" bar" , signedbv_typet{16 }}};
51
- struct_typet struct_type{components};
52
- type_symbolt type_symbol{" my_structt" , struct_type, ID_C};
53
- auto test = struct_encoding_test_environmentt::make ();
54
- test.symbol_table .insert (type_symbol);
55
- struct_tag_typet struct_tag{type_symbol.name };
56
- const auto index_type = signedbv_typet{32 };
57
- const auto array_size = from_integer (5 , index_type);
58
- array_typet array_of_struct{struct_tag, array_size};
59
- array_typet expected_encoded_array{bv_typet{24 }, array_size};
60
- REQUIRE (
61
- test.struct_encoding .encode (array_of_struct) == expected_encoded_array);
62
- }
63
-
64
- TEST_CASE (
65
- " struct encoding of array of array of structs" ,
66
- " [core][smt2_incremental]" )
67
- {
68
- const struct_union_typet::componentst components{
69
- {" foo" , unsignedbv_typet{8 }}, {" bar" , signedbv_typet{16 }}};
70
- struct_typet struct_type{components};
71
- type_symbolt type_symbol{" my_structt" , struct_type, ID_C};
72
- auto test = struct_encoding_test_environmentt::make ();
73
- test.symbol_table .insert (type_symbol);
74
- struct_tag_typet struct_tag{type_symbol.name };
75
- const auto index_type = signedbv_typet{32 };
76
- const auto array_size_inner = from_integer (4 , index_type);
77
- const auto array_size_outer = from_integer (2 , index_type);
78
- array_typet array_of_struct{struct_tag, array_size_inner};
79
- array_typet array_of_array_of_struct{array_of_struct, array_size_outer};
80
- array_typet expected_encoded_array{
81
- array_typet{bv_typet{24 }, array_size_inner}, array_size_outer};
82
- REQUIRE (
83
- test.struct_encoding .encode (array_of_array_of_struct) ==
84
- expected_encoded_array);
44
+ SECTION (" direct struct_tag_type encoding" )
45
+ {
46
+ REQUIRE (test.struct_encoding .encode (struct_tag) == bv_typet{24 });
47
+ }
48
+ SECTION (" array of structs encoding" )
49
+ {
50
+ const auto index_type = signedbv_typet{32 };
51
+ const auto array_size = from_integer (5 , index_type);
52
+ array_typet array_of_struct{struct_tag, array_size};
53
+ array_typet expected_encoded_array{bv_typet{24 }, array_size};
54
+ REQUIRE (
55
+ test.struct_encoding .encode (array_of_struct) == expected_encoded_array);
56
+ }
57
+ SECTION (" array of array of structs encoding" )
58
+ {
59
+ const auto index_type = signedbv_typet{32 };
60
+ const auto array_size_inner = from_integer (4 , index_type);
61
+ const auto array_size_outer = from_integer (2 , index_type);
62
+ array_typet array_of_struct{struct_tag, array_size_inner};
63
+ array_typet array_of_array_of_struct{array_of_struct, array_size_outer};
64
+ array_typet expected_encoded_array{
65
+ array_typet{bv_typet{24 }, array_size_inner}, array_size_outer};
66
+ REQUIRE (
67
+ test.struct_encoding .encode (array_of_array_of_struct) ==
68
+ expected_encoded_array);
69
+ }
85
70
}
0 commit comments