@@ -298,6 +298,16 @@ TEST_CASE("nondet_initializer c_enum", "[core][util][expr_initializer]")
298
298
create_tag_populate_env (enum_type, test.symbol_table );
299
299
const auto tag_result =
300
300
nondet_initializer (c_enum_tag_type, test.loc , test.ns );
301
+
302
+ SECTION (" zero_initializer works" )
303
+ {
304
+ // TODO: zero_initializer works initializing with 0. (see structure above)
305
+ }
306
+ SECTION (" expr_initializer calls duplicate_per_byte" )
307
+ {
308
+ // TODO: duplicate_per_byte is tested separately. Here we should check that
309
+ // expr_initializer calls duplicate_per_byte. (see structure above)
310
+ }
301
311
}
302
312
303
313
TEST_CASE (
@@ -318,6 +328,16 @@ TEST_CASE(
318
328
array_typet{
319
329
signedbv_typet{8 }, from_integer (elem_count, signedbv_typet{8 })}};
320
330
REQUIRE (result.value () == expected);
331
+
332
+ SECTION (" zero_initializer works" )
333
+ {
334
+ // TODO: zero_initializer works initializing with 0. (see structure above)
335
+ }
336
+ SECTION (" expr_initializer calls duplicate_per_byte" )
337
+ {
338
+ // TODO: duplicate_per_byte is tested separately. Here we should check that
339
+ // expr_initializer calls duplicate_per_byte. (see structure above)
340
+ }
321
341
}
322
342
323
343
TEST_CASE (
@@ -335,6 +355,16 @@ TEST_CASE(
335
355
inner_type, side_effect_expr_nondett{signedbv_typet{8 }, test.loc }},
336
356
test.loc };
337
357
REQUIRE (result.value () == expected);
358
+
359
+ SECTION (" zero_initializer works" )
360
+ {
361
+ // TODO: zero_initializer works initializing with 0. (see structure above)
362
+ }
363
+ SECTION (" expr_initializer calls duplicate_per_byte" )
364
+ {
365
+ // TODO: duplicate_per_byte is tested separately. Here we should check that
366
+ // expr_initializer calls duplicate_per_byte. (see structure above)
367
+ }
338
368
}
339
369
340
370
TEST_CASE (
@@ -364,6 +394,16 @@ TEST_CASE(
364
394
signedbv_typet{8 }, from_integer (elem_count, signedbv_typet{8 })},
365
395
from_integer (elem_count, signedbv_typet{8 })}};
366
396
REQUIRE (result.value () == expected);
397
+
398
+ SECTION (" zero_initializer works" )
399
+ {
400
+ // TODO: zero_initializer works initializing with 0. (see structure above)
401
+ }
402
+ SECTION (" expr_initializer calls duplicate_per_byte" )
403
+ {
404
+ // TODO: duplicate_per_byte is tested separately. Here we should check that
405
+ // expr_initializer calls duplicate_per_byte. (see structure above)
406
+ }
367
407
}
368
408
369
409
TEST_CASE (
@@ -398,6 +438,16 @@ TEST_CASE(
398
438
const struct_exprt expected_inner_struct_tag_expr{
399
439
expected_inner_struct_fields, inner_struct_tag_type};
400
440
REQUIRE (tag_result.value () == expected_inner_struct_tag_expr);
441
+
442
+ SECTION (" zero_initializer works" )
443
+ {
444
+ // TODO: zero_initializer works initializing with 0. (see structure above)
445
+ }
446
+ SECTION (" expr_initializer calls duplicate_per_byte" )
447
+ {
448
+ // TODO: duplicate_per_byte is tested separately. Here we should check that
449
+ // expr_initializer calls duplicate_per_byte. (see structure above)
450
+ }
401
451
}
402
452
403
453
TEST_CASE (" nondet_initializer union type" , " [core][util][expr_initializer]" )
@@ -429,6 +479,16 @@ TEST_CASE("nondet_initializer union type", "[core][util][expr_initializer]")
429
479
side_effect_expr_nondett{signedbv_typet{256 }, test.loc },
430
480
union_tag_type};
431
481
REQUIRE (tag_result.value () == expected_union_tag);
482
+
483
+ SECTION (" zero_initializer works" )
484
+ {
485
+ // TODO: zero_initializer works initializing with 0. (see structure above)
486
+ }
487
+ SECTION (" expr_initializer calls duplicate_per_byte" )
488
+ {
489
+ // TODO: duplicate_per_byte is tested separately. Here we should check that
490
+ // expr_initializer calls duplicate_per_byte. (see structure above)
491
+ }
432
492
}
433
493
434
494
TEST_CASE (
@@ -445,6 +505,16 @@ TEST_CASE(
445
505
const union_typet union_type{union_components};
446
506
const auto result = nondet_initializer (union_type, test.loc , test.ns );
447
507
REQUIRE_FALSE (result.has_value ());
508
+
509
+ SECTION (" zero_initializer works" )
510
+ {
511
+ // TODO: zero_initializer works initializing with 0. (see structure above)
512
+ }
513
+ SECTION (" expr_initializer calls duplicate_per_byte" )
514
+ {
515
+ // TODO: duplicate_per_byte is tested separately. Here we should check that
516
+ // expr_initializer calls duplicate_per_byte. (see structure above)
517
+ }
448
518
}
449
519
450
520
TEST_CASE (" nondet_initializer string type" , " [core][util][expr_initializer]" )
@@ -455,4 +525,14 @@ TEST_CASE("nondet_initializer string type", "[core][util][expr_initializer]")
455
525
REQUIRE (result.has_value ());
456
526
const side_effect_expr_nondett expected_string{string_typet{}, test.loc };
457
527
REQUIRE (result.value () == expected_string);
528
+
529
+ SECTION (" zero_initializer works" )
530
+ {
531
+ // TODO: zero_initializer works initializing with 0. (see structure above)
532
+ }
533
+ SECTION (" expr_initializer calls duplicate_per_byte" )
534
+ {
535
+ // TODO: duplicate_per_byte is tested separately. Here we should check that
536
+ // expr_initializer calls duplicate_per_byte. (see structure above)
537
+ }
458
538
}
0 commit comments