Skip to content

Commit 1fe0796

Browse files
martinmartin
martin
authored and
martin
committed
Convert various older domains to use the more recent ait API.
This is mostly using accessor functions rather than directly using inherited members but it allows a slightly greater degree of independence.
1 parent afe32b7 commit 1fe0796

File tree

3 files changed

+17
-15
lines changed

3 files changed

+17
-15
lines changed

src/analyses/constant_propagator.cpp

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -592,43 +592,45 @@ void constant_propagator_ait::replace(
592592
{
593593
Forall_goto_program_instructions(it, goto_function.body)
594594
{
595-
state_mapt::iterator s_it=state_map.find(it);
595+
// Works because this is a location (but not history) sensitive domain
596+
const constant_propagator_domaint &d = (*this)[it];
596597

597-
if(s_it==state_map.end())
598+
if(d.is_bottom())
598599
continue;
599600

600-
replace_types_rec(s_it->second.values.replace_const, it->code);
601-
replace_types_rec(s_it->second.values.replace_const, it->guard);
601+
replace_types_rec(d.values.replace_const, it->code);
602+
replace_types_rec(d.values.replace_const, it->guard);
602603

603604
if(it->is_goto() || it->is_assume() || it->is_assert())
604605
{
605-
s_it->second.partial_evaluate(it->guard, ns);
606+
d.partial_evaluate(it->guard, ns);
606607
}
607608
else if(it->is_assign())
608609
{
609610
exprt &rhs=to_code_assign(it->code).rhs();
610-
s_it->second.partial_evaluate(rhs, ns);
611+
d.partial_evaluate(rhs, ns);
612+
611613
if(rhs.id()==ID_constant)
612614
rhs.add_source_location()=it->code.op0().source_location();
613615
}
614616
else if(it->is_function_call())
615617
{
616618
exprt &function = to_code_function_call(it->code).function();
617-
s_it->second.partial_evaluate(function, ns);
619+
d.partial_evaluate(function, ns);
618620

619621
exprt::operandst &args=
620622
to_code_function_call(it->code).arguments();
621623

622624
for(auto &arg : args)
623625
{
624-
s_it->second.partial_evaluate(arg, ns);
626+
d.partial_evaluate(arg, ns);
625627
}
626628
}
627629
else if(it->is_other())
628630
{
629631
if(it->code.get_statement()==ID_expression)
630632
{
631-
s_it->second.partial_evaluate(it->code, ns);
633+
d.partial_evaluate(it->code, ns);
632634
}
633635
}
634636
}

src/analyses/dependence_graph.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -307,9 +307,9 @@ void dependence_grapht::add_dep(
307307
goto_programt::const_targett from,
308308
goto_programt::const_targett to)
309309
{
310-
const node_indext n_from=state_map[from].get_node_id();
310+
const node_indext n_from = (*this)[from].get_node_id();
311311
assert(n_from<size());
312-
const node_indext n_to=state_map[to].get_node_id();
312+
const node_indext n_to = (*this)[to].get_node_id();
313313
assert(n_to<size());
314314

315315
// add_edge is redundant as the subsequent operations also insert

src/analyses/invariant_propagation.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ void invariant_propagationt::initialize(const goto_programt &goto_program)
206206

207207
forall_goto_program_instructions(it, goto_program)
208208
{
209-
invariant_sett &s=state_map[it].invariant_set;
209+
invariant_sett &s = (*this)[it].invariant_set;
210210

211211
if(it==goto_program.instructions.begin())
212212
s.make_true();
@@ -243,11 +243,11 @@ void invariant_propagationt::simplify(goto_programt &goto_program)
243243
continue;
244244

245245
// find invariant set
246-
state_mapt::const_iterator s_it=state_map.find(i_it);
247-
if(s_it==state_map.end())
246+
const auto &d = (*this)[i_it];
247+
if(d.is_bottom())
248248
continue;
249249

250-
const invariant_sett &invariant_set=s_it->second.invariant_set;
250+
const invariant_sett &invariant_set = d.invariant_set;
251251

252252
exprt simplified_guard(i_it->guard);
253253

0 commit comments

Comments
 (0)