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