@@ -362,16 +362,16 @@ class interval_evaluator
362
362
return make_top<interval_abstract_valuet>(expression.type ());
363
363
364
364
if (expression.id () == ID_if)
365
- return interval_evaluate_conditional (interval_operands);
365
+ return evaluate_conditional (interval_operands);
366
366
367
367
if (num_operands == 1 )
368
- return interval_evaluate_unary_expr (interval_operands);
368
+ return evaluate_unary_expr (interval_operands);
369
369
370
- constant_interval_exprt result = interval_operands[0 ]-> to_interval () ;
370
+ constant_interval_exprt result = interval_operands[0 ];
371
371
372
372
for (size_t opIndex = 1 ; opIndex != interval_operands.size (); ++opIndex)
373
373
{
374
- auto &interval_next = interval_operands[opIndex]-> to_interval () ;
374
+ auto &interval_next = interval_operands[opIndex];
375
375
result = result.eval (expression.id (), interval_next);
376
376
}
377
377
@@ -381,22 +381,22 @@ class interval_evaluator
381
381
return make_interval (result);
382
382
}
383
383
384
- std::vector<interval_abstract_value_pointert > operands_as_intervals () const
384
+ std::vector<constant_interval_exprt > operands_as_intervals () const
385
385
{
386
- std::vector<interval_abstract_value_pointert > interval_operands;
386
+ std::vector<constant_interval_exprt > interval_operands;
387
387
388
388
for (const auto &op : operands)
389
389
{
390
390
auto iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(op);
391
391
if (!iav)
392
392
{
393
- // The operand isn't an interval - if it's an integral constant we can
394
- // convert it into an interval.
393
+ // The operand isn't an interval
394
+ // if it's an integral constant we can convert it into an interval.
395
395
if (constant_interval_exprt::is_int (op->type ()))
396
396
{
397
397
const auto op_as_constant = op->to_constant ();
398
398
if (op_as_constant.is_nil ())
399
- return std::vector<interval_abstract_value_pointert >();
399
+ return std::vector<constant_interval_exprt >();
400
400
401
401
iav = make_interval (op_as_constant);
402
402
}
@@ -405,19 +405,18 @@ class interval_evaluator
405
405
}
406
406
407
407
if (iav)
408
- interval_operands.push_back (iav);
408
+ interval_operands.push_back (iav-> to_interval () );
409
409
}
410
410
411
411
return interval_operands;
412
412
}
413
413
414
- abstract_object_pointert interval_evaluate_conditional (
415
- const std::vector<interval_abstract_value_pointert> &interval_operands)
416
- const
414
+ abstract_object_pointert evaluate_conditional (
415
+ const std::vector<constant_interval_exprt> &interval_operands) const
417
416
{
418
- auto const &condition_interval = interval_operands[0 ]-> to_interval () ;
419
- auto const &true_interval = interval_operands[1 ]-> to_interval () ;
420
- auto const &false_interval = interval_operands[2 ]-> to_interval () ;
417
+ auto const &condition_interval = interval_operands[0 ];
418
+ auto const &true_interval = interval_operands[1 ];
419
+ auto const &false_interval = interval_operands[2 ];
421
420
422
421
auto condition_result = condition_interval.is_definitely_true ();
423
422
@@ -436,12 +435,10 @@ class interval_evaluator
436
435
: make_interval (false_interval);
437
436
}
438
437
439
- abstract_object_pointert interval_evaluate_unary_expr (
440
- const std::vector<interval_abstract_value_pointert> &interval_operands)
441
- const
438
+ abstract_object_pointert evaluate_unary_expr (
439
+ const std::vector<constant_interval_exprt> &interval_operands) const
442
440
{
443
- const constant_interval_exprt &operand_expr =
444
- interval_operands[0 ]->to_interval ();
441
+ const constant_interval_exprt &operand_expr = interval_operands[0 ];
445
442
446
443
if (expression.id () == ID_typecast)
447
444
{
@@ -509,12 +506,12 @@ class value_set_evaluator
509
506
private:
510
507
abstract_object_pointert transform () const
511
508
{
512
- auto collective_operands = unwrap_operands ();
509
+ auto ranges = operands_as_ranges ();
513
510
514
511
if (expression.id () == ID_if)
515
- return value_set_evaluate_conditional (collective_operands );
512
+ return evaluate_conditional (ranges );
516
513
517
- auto resulting_objects = evaluate_each_combination (collective_operands );
514
+ auto resulting_objects = evaluate_each_combination (ranges );
518
515
519
516
return resolve_values (resulting_objects);
520
517
}
@@ -565,7 +562,7 @@ class value_set_evaluator
565
562
return rewritten_expr;
566
563
}
567
564
568
- std::vector<value_ranget> unwrap_operands () const
565
+ std::vector<value_ranget> operands_as_ranges () const
569
566
{
570
567
auto unwrapped = std::vector<value_ranget>{};
571
568
@@ -633,7 +630,7 @@ class value_set_evaluator
633
630
}
634
631
635
632
static abstract_object_pointert
636
- value_set_evaluate_conditional (const std::vector<value_ranget> &ops)
633
+ evaluate_conditional (const std::vector<value_ranget> &ops)
637
634
{
638
635
auto const &condition = ops[0 ];
639
636
0 commit comments