@@ -372,34 +372,33 @@ static abstract_environmentt get_value_set_abstract_environment()
372
372
return abstract_environmentt{};
373
373
}
374
374
375
- TEST_CASE (
376
- " Eval on an constant gives us that constant" , VALUE_SET_TEST_TAGS)
375
+ TEST_CASE (" Eval on an constant gives us that constant" , VALUE_SET_TEST_TAGS)
377
376
{
378
377
const auto environment = get_value_set_abstract_environment ();
379
378
namespacet ns{symbol_tablet{}};
380
- const auto zero =
381
- from_integer (0 , signedbv_typet{32 });
379
+ const auto zero = from_integer (0 , signedbv_typet{32 });
382
380
const auto eval_result = environment.eval (zero, ns);
383
381
REQUIRE (eval_result != nullptr );
384
382
REQUIRE (!eval_result->is_top ());
385
383
REQUIRE (!eval_result->is_bottom ());
386
384
const auto eval_result_as_value_set =
387
- std::dynamic_pointer_cast<const value_set_abstract_valuet>(eval_result->unwrap_context ());
385
+ std::dynamic_pointer_cast<const value_set_abstract_valuet>(
386
+ eval_result->unwrap_context ());
388
387
REQUIRE (eval_result_as_value_set != nullptr );
389
388
REQUIRE (eval_result_as_value_set->get_values ().size () == 1 );
390
- REQUIRE_THAT (eval_result_as_value_set->get_values (),
391
- ContainsAllOf{zero});
389
+ REQUIRE_THAT (eval_result_as_value_set->get_values (), ContainsAllOf{zero});
392
390
}
393
391
394
392
TEST_CASE (
395
- " Eval on a plus expression with constant operands gives us the result of that plus" ,
393
+ " Eval on a plus expression with constant operands gives us the result of "
394
+ " that plus" ,
396
395
VALUE_SET_TEST_TAGS)
397
396
{
398
397
const auto environment = get_value_set_abstract_environment ();
399
398
namespacet ns{symbol_tablet{}};
400
399
const auto s32_type = signedbv_typet{32 };
401
- const auto three =from_integer (3 , s32_type);
402
- const auto five =from_integer (5 , s32_type);
400
+ const auto three = from_integer (3 , s32_type);
401
+ const auto five = from_integer (5 , s32_type);
403
402
const auto three_plus_five = plus_exprt{three, five};
404
403
405
404
auto eval_result = environment.eval (three_plus_five, ns);
@@ -408,15 +407,17 @@ TEST_CASE(
408
407
REQUIRE (!eval_result->is_bottom ());
409
408
410
409
const auto eval_result_as_value_set =
411
- std::dynamic_pointer_cast<const value_set_abstract_valuet>(eval_result->unwrap_context ());
410
+ std::dynamic_pointer_cast<const value_set_abstract_valuet>(
411
+ eval_result->unwrap_context ());
412
412
REQUIRE (eval_result_as_value_set != nullptr );
413
413
const auto eight = from_integer (8 , s32_type);
414
414
REQUIRE (eval_result_as_value_set->get_values ().size () == 1 );
415
415
REQUIRE_THAT (eval_result_as_value_set->get_values (), ContainsAllOf{eight});
416
416
}
417
417
418
418
TEST_CASE (
419
- " Eval on a multiply expression on symbols gives us the results of that multiplication" ,
419
+ " Eval on a multiply expression on symbols gives us the results of that "
420
+ " multiplication" ,
420
421
VALUE_SET_TEST_TAGS)
421
422
{
422
423
auto environment = get_value_set_abstract_environment ();
@@ -445,31 +446,32 @@ TEST_CASE(
445
446
const auto six = from_integer (6 , s32_type);
446
447
447
448
const auto three_or_five = std::make_shared<const value_set_abstract_valuet>(
448
- s32_type,
449
- value_set_abstract_valuet::valuest{three, five});
449
+ s32_type, value_set_abstract_valuet::valuest{three, five});
450
450
environment.assign (a_symbol.symbol_expr (), three_or_five, ns);
451
451
452
452
const auto four_or_six = std::make_shared<const value_set_abstract_valuet>(
453
- s32_type,
454
- value_set_abstract_valuet::valuest{four, six});
453
+ s32_type, value_set_abstract_valuet::valuest{four, six});
455
454
environment.assign (b_symbol.symbol_expr (), four_or_six, ns);
456
455
457
- const auto a_times_b = mult_exprt{a_symbol.symbol_expr (), b_symbol.symbol_expr ()};
456
+ const auto a_times_b =
457
+ mult_exprt{a_symbol.symbol_expr (), b_symbol.symbol_expr ()};
458
458
459
459
const auto eval_result = environment.eval (a_times_b, ns);
460
460
REQUIRE (eval_result != nullptr );
461
461
REQUIRE (!eval_result->is_top ());
462
462
REQUIRE (!eval_result->is_bottom ());
463
463
464
464
const auto eval_result_as_value_set =
465
- std::dynamic_pointer_cast<const value_set_abstract_valuet>(eval_result->unwrap_context ());
465
+ std::dynamic_pointer_cast<const value_set_abstract_valuet>(
466
+ eval_result->unwrap_context ());
466
467
REQUIRE (eval_result_as_value_set != nullptr );
467
468
REQUIRE (eval_result_as_value_set->get_values ().size () == 4 );
468
469
469
470
const auto twelve = from_integer (12 , s32_type);
470
471
const auto eighteen = from_integer (18 , s32_type);
471
472
const auto twenty = from_integer (20 , s32_type);
472
473
const auto twentyfour = from_integer (30 , s32_type);
473
- REQUIRE_THAT (eval_result_as_value_set->get_values (),
474
- ContainsAllOf (twelve, eighteen, twenty, twentyfour));
475
- }
474
+ REQUIRE_THAT (
475
+ eval_result_as_value_set->get_values (),
476
+ ContainsAllOf (twelve, eighteen, twenty, twentyfour));
477
+ }
0 commit comments