@@ -359,7 +359,8 @@ void goto_symext::merge_value_sets(
359
359
static void for_each2 (
360
360
const std::map<irep_idt, std::pair<ssa_exprt, unsigned >> &first_map,
361
361
const std::map<irep_idt, std::pair<ssa_exprt, unsigned >> &second_map,
362
- std::function<void (const irep_idt &, const ssa_exprt &, unsigned , unsigned )> f)
362
+ std::function<void (const irep_idt &, const ssa_exprt &, unsigned , unsigned )>
363
+ f)
363
364
{
364
365
auto second_it = second_map.begin ();
365
366
for (const auto &first_pair : first_map)
@@ -399,7 +400,8 @@ static void for_each2(
399
400
// / \param[out] target: equation that will receive the resulting assignment
400
401
// / \param l1_identifier: name of the variable to merge
401
402
// / \param ssa: SSA expression corresponding to \p l1_identifier
402
- // / \param goto_count: current level 2 count in \p goto_state of \p l1_identifier
403
+ // / \param goto_count: current level 2 count in \p goto_state of
404
+ // / \p l1_identifier
403
405
// / \param dest_count: level 2 count in \p dest_state of \p l1_identifier
404
406
static void merge_names (
405
407
const goto_symext::statet::goto_statet &goto_state,
@@ -417,7 +419,7 @@ static void merge_names(
417
419
{
418
420
const irep_idt &obj_identifier = ssa.get_object_name ();
419
421
420
- if (obj_identifier== guard_identifier)
422
+ if (obj_identifier == guard_identifier)
421
423
return ; // just a guard, don't bother
422
424
423
425
if (goto_count == dest_count)
@@ -427,12 +429,12 @@ static void merge_names(
427
429
428
430
// shared variables are renamed on every access anyway, we don't need to
429
431
// merge anything
430
- const symbolt &symbol= ns.lookup (obj_identifier);
432
+ const symbolt &symbol = ns.lookup (obj_identifier);
431
433
432
434
// shared?
433
435
if (
434
436
dest_state.atomic_section_id == 0 && dest_state.threads .size () >= 2 &&
435
- (symbol.is_shared () || (dest_state.dirty )(symbol.name )))
437
+ (symbol.is_shared () || (dest_state.dirty )(symbol.name )))
436
438
return ; // no phi nodes for shared stuff
437
439
438
440
// don't merge (thread-)locals across different threads, which
@@ -441,7 +443,7 @@ static void merge_names(
441
443
// once the thread is executed)
442
444
if (
443
445
!ssa.get_level_0 ().empty () &&
444
- ssa.get_level_0 () != std::to_string (dest_state.source .thread_nr ))
446
+ ssa.get_level_0 () != std::to_string (dest_state.source .thread_nr ))
445
447
return ;
446
448
447
449
exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
@@ -450,7 +452,7 @@ static void merge_names(
450
452
const auto p_it = goto_state.propagation .find (l1_identifier);
451
453
452
454
if (p_it != goto_state.propagation .end ())
453
- goto_state_rhs= p_it->second ;
455
+ goto_state_rhs = p_it->second ;
454
456
else
455
457
to_ssa_expr (goto_state_rhs).set_level_2 (goto_count);
456
458
}
@@ -459,7 +461,7 @@ static void merge_names(
459
461
const auto p_it = dest_state.propagation .find (l1_identifier);
460
462
461
463
if (p_it != dest_state.propagation .end ())
462
- dest_state_rhs= p_it->second ;
464
+ dest_state_rhs = p_it->second ;
463
465
else
464
466
to_ssa_expr (dest_state_rhs).set_level_2 (dest_count);
465
467
}
@@ -471,9 +473,9 @@ static void merge_names(
471
473
// 2. Either identifier is of generation zero, and so hasn't been
472
474
// initialized and therefor an invalid target.
473
475
if (dest_state.guard .is_false ())
474
- rhs= goto_state_rhs;
476
+ rhs = goto_state_rhs;
475
477
else if (goto_state.guard .is_false ())
476
- rhs= dest_state_rhs;
478
+ rhs = dest_state_rhs;
477
479
else if (goto_count == 0 )
478
480
{
479
481
rhs = dest_state_rhs;
@@ -484,28 +486,29 @@ static void merge_names(
484
486
}
485
487
else
486
488
{
487
- rhs= if_exprt (diff_guard.as_expr (), goto_state_rhs, dest_state_rhs);
489
+ rhs = if_exprt (diff_guard.as_expr (), goto_state_rhs, dest_state_rhs);
488
490
if (do_simplify)
489
491
simplify (rhs, ns);
490
492
}
491
493
492
494
ssa_exprt new_lhs = ssa;
493
- const bool record_events= dest_state.record_events ;
494
- dest_state.record_events = false ;
495
+ const bool record_events = dest_state.record_events ;
496
+ dest_state.record_events = false ;
495
497
dest_state.assignment (new_lhs, rhs, ns, true , true );
496
- dest_state.record_events = record_events;
498
+ dest_state.record_events = record_events;
497
499
498
500
log .conditional_output (
499
- log .debug (),
500
- [ns, &new_lhs](messaget::mstreamt &mstream) {
501
- mstream << " Assignment to " << new_lhs.get_identifier ()
502
- << " [" << pointer_offset_bits (new_lhs.type (), ns).value_or (0 ) << " bits]"
501
+ log .debug (), [ns, &new_lhs](messaget::mstreamt &mstream) {
502
+ mstream << " Assignment to " << new_lhs.get_identifier () << " ["
503
+ << pointer_offset_bits (new_lhs.type (), ns).value_or (0 ) << " bits]"
503
504
<< messaget::eom;
504
505
});
505
506
506
507
target.assignment (
507
508
true_exprt (),
508
- new_lhs, new_lhs, new_lhs.get_original_expr (),
509
+ new_lhs,
510
+ new_lhs,
511
+ new_lhs.get_original_expr (),
509
512
rhs,
510
513
dest_state.source ,
511
514
symex_targett::assignment_typet::PHI);
@@ -516,22 +519,23 @@ void goto_symext::phi_function(
516
519
statet &dest_state)
517
520
{
518
521
guardt diff_guard;
519
- if (goto_state.level2_current_names .empty () &&
520
- dest_state.level2 .current_names .empty ())
522
+ if (
523
+ goto_state.level2_current_names .empty () &&
524
+ dest_state.level2 .current_names .empty ())
521
525
return ;
522
526
523
- diff_guard= goto_state.guard ;
527
+ diff_guard = goto_state.guard ;
524
528
// this gets the diff between the guards
525
- diff_guard-= dest_state.guard ;
529
+ diff_guard -= dest_state.guard ;
526
530
527
531
for_each2 (
528
532
goto_state.level2_current_names ,
529
533
dest_state.level2 .current_names ,
530
- [&](const irep_idt &l1_identifier,
531
- const ssa_exprt &ssa ,
532
- unsigned goto_count ,
533
- unsigned dest_count)
534
- {
534
+ [&](
535
+ const irep_idt &l1_identifier ,
536
+ const ssa_exprt &ssa ,
537
+ unsigned goto_count,
538
+ unsigned dest_count) {
535
539
merge_names (
536
540
goto_state,
537
541
dest_state,
0 commit comments