@@ -32,7 +32,7 @@ TEST_CASE(
3232 REQUIRE (test.struct_encoding .encode (input) == input);
3333}
3434
35- TEST_CASE (" struct encoding of struct_tag_type " , " [core][smt2_incremental]" )
35+ TEST_CASE (" struct encoding of types " , " [core][smt2_incremental]" )
3636{
3737 const struct_union_typet::componentst components{
3838 {" foo" , unsignedbv_typet{8 }}, {" bar" , signedbv_typet{16 }}};
@@ -41,45 +41,30 @@ TEST_CASE("struct encoding of struct_tag_type", "[core][smt2_incremental]")
4141 auto test = struct_encoding_test_environmentt::make ();
4242 test.symbol_table .insert (type_symbol);
4343 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+ }
8570}
0 commit comments