Skip to content

Commit f9684b4

Browse files
tautschnigtautschnig
authored
Merge pull request #6852 from diffblue/remove_get_set_condition
remove goto_programt::get_ and set_condition
2 parents 58d64d8 + a25657d commit f9684b4

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

60 files changed

+139
-184
lines changed

‎src/analyses/constant_propagator.cpp

+5-5
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,7 @@ void constant_propagator_domaint::transform(
171171
}
172172
else if(from->is_assume())
173173
{
174-
two_way_propagate_rec(from->get_condition(), ns, cp);
174+
two_way_propagate_rec(from->condition(), ns, cp);
175175
}
176176
else if(from->is_goto())
177177
{
@@ -180,9 +180,9 @@ void constant_propagator_domaint::transform(
180180
// Comparing iterators is safe as the target must be within the same list
181181
// of instructions because this is a GOTO.
182182
if(from->get_target()==to)
183-
g = from->get_condition();
183+
g = from->condition();
184184
else
185-
g = not_exprt(from->get_condition());
185+
g = not_exprt(from->condition());
186186
partial_evaluate(values, g, ns);
187187
if(g.is_false())
188188
values.set_to_bottom();
@@ -762,10 +762,10 @@ void constant_propagator_ait::replace(
762762

763763
if(it->is_goto() || it->is_assume() || it->is_assert())
764764
{
765-
exprt c = it->get_condition();
765+
exprt c = it->condition();
766766
replace_types_rec(d.values.replace_const, c);
767767
if(!constant_propagator_domaint::partial_evaluate(d.values, c, ns))
768-
it->set_condition(c);
768+
it->condition_nonconst() = c;
769769
}
770770
else if(it->is_assign())
771771
{

‎src/analyses/custom_bitvector_analysis.cpp

+4-5
Original file line numberDiff line numberDiff line change
@@ -517,9 +517,9 @@ void custom_bitvector_domaint::transform(
517517
break;
518518

519519
case GOTO:
520-
if(has_get_must_or_may(instruction.get_condition()))
520+
if(has_get_must_or_may(instruction.condition()))
521521
{
522-
exprt guard = instruction.get_condition();
522+
exprt guard = instruction.condition();
523523

524524
// Comparing iterators is safe as the target must be within the same list
525525
// of instructions because this is a GOTO.
@@ -790,16 +790,15 @@ void custom_bitvector_analysist::check(
790790

791791
if(i_it->is_assert())
792792
{
793-
if(!custom_bitvector_domaint::has_get_must_or_may(
794-
i_it->get_condition()))
793+
if(!custom_bitvector_domaint::has_get_must_or_may(i_it->condition()))
795794
{
796795
continue;
797796
}
798797

799798
if(operator[](i_it).has_values.is_false())
800799
continue;
801800

802-
exprt tmp = eval(i_it->get_condition(), i_it);
801+
exprt tmp = eval(i_it->condition(), i_it);
803802
const namespacet ns(goto_model.symbol_table);
804803
result = simplify_expr(std::move(tmp), ns);
805804

‎src/analyses/flow_insensitive_analysis.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,9 @@ exprt flow_insensitive_abstract_domain_baset::get_guard(
2323
if(!from->is_goto())
2424
return true_exprt();
2525
else if(std::next(from) == to)
26-
return boolean_negate(from->get_condition());
26+
return boolean_negate(from->condition());
2727
else
28-
return from->get_condition();
28+
return from->condition();
2929
}
3030

3131
exprt flow_insensitive_abstract_domain_baset::get_return_lhs(locationt to) const

‎src/analyses/goto_rw.cpp

+1-4
Original file line numberDiff line numberDiff line change
@@ -867,10 +867,7 @@ void goto_rw(
867867
case ASSUME:
868868
case ASSERT:
869869
rw_set.get_objects_rec(
870-
function,
871-
target,
872-
rw_range_sett::get_modet::READ,
873-
target->get_condition());
870+
function, target, rw_range_sett::get_modet::READ, target->condition());
874871
break;
875872

876873
case SET_RETURN_VALUE:

‎src/analyses/interval_analysis.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ void instrument_intervals(
4646
{
4747
goto_programt::const_targett previous = std::prev(i_it);
4848

49-
if(previous->is_goto() && !previous->get_condition().is_true())
49+
if(previous->is_goto() && !previous->condition().is_true())
5050
{
5151
// we follow a branch, instrument
5252
}

‎src/analyses/interval_domain.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -91,15 +91,15 @@ void interval_domaint::transform(
9191
if(from->get_target() != next) // If equal then a skip
9292
{
9393
if(next == to)
94-
assume(not_exprt(instruction.get_condition()), ns);
94+
assume(not_exprt(instruction.condition()), ns);
9595
else
96-
assume(instruction.get_condition(), ns);
96+
assume(instruction.condition(), ns);
9797
}
9898
break;
9999
}
100100

101101
case ASSUME:
102-
assume(instruction.get_condition(), ns);
102+
assume(instruction.condition(), ns);
103103
break;
104104

105105
case FUNCTION_CALL:

‎src/analyses/invariant_propagation.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -264,7 +264,7 @@ void invariant_propagationt::simplify(goto_programt &goto_program)
264264

265265
const invariant_sett &invariant_set = d.invariant_set;
266266

267-
exprt simplified_guard(i_it->get_condition());
267+
exprt simplified_guard(i_it->condition());
268268

269269
invariant_set.simplify(simplified_guard);
270270
::simplify(simplified_guard, ns);

‎src/analyses/invariant_set_domain.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ void invariant_set_domaint::transform(
3131
{
3232
// Comparing iterators is safe as the target must be within the same list
3333
// of instructions because this is a GOTO.
34-
exprt tmp(from_l->get_condition());
34+
exprt tmp(from_l->condition());
3535

3636
if(std::next(from_l) == to_l)
3737
tmp = boolean_negate(tmp);
@@ -44,7 +44,7 @@ void invariant_set_domaint::transform(
4444
case ASSERT:
4545
case ASSUME:
4646
{
47-
exprt tmp(from_l->get_condition());
47+
exprt tmp(from_l->condition());
4848
simplify(tmp, ns);
4949
invariant_set.strengthen(tmp);
5050
}

‎src/analyses/local_cfg.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ void local_cfgt::build(const goto_programt &goto_program)
3535
switch(instruction.type())
3636
{
3737
case GOTO:
38-
if(!instruction.get_condition().is_true())
38+
if(!instruction.condition().is_true())
3939
node.successors.push_back(loc_nr+1);
4040

4141
for(const auto &target : instruction.targets)

‎src/analyses/local_safe_pointers.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
127127

128128
// Possible checks:
129129
case ASSUME:
130-
if(auto assume_check = get_null_checked_expr(instruction.get_condition()))
130+
if(auto assume_check = get_null_checked_expr(instruction.condition()))
131131
{
132132
if(assume_check->checked_when_taken)
133133
checked_expressions.insert(assume_check->checked_expr);
@@ -150,7 +150,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
150150
{
151151
if(
152152
auto conditional_check =
153-
get_null_checked_expr(instruction.get_condition()))
153+
get_null_checked_expr(instruction.condition()))
154154
{
155155
// Add the GOTO condition to either the target or current state,
156156
// as appropriate:

‎src/analyses/static_analysis.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -27,9 +27,9 @@ exprt static_analysis_baset::get_guard(
2727
if(!from->is_goto())
2828
return true_exprt();
2929
else if(std::next(from) == to)
30-
return boolean_negate(from->get_condition());
30+
return boolean_negate(from->condition());
3131
else
32-
return from->get_condition();
32+
return from->condition();
3333
}
3434

3535
exprt static_analysis_baset::get_return_lhs(locationt to)

‎src/ansi-c/goto_check_c.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -2085,7 +2085,7 @@ void goto_check_ct::goto_check(
20852085

20862086
if(i.has_condition())
20872087
{
2088-
check(i.get_condition());
2088+
check(i.condition());
20892089
}
20902090

20912091
// magic ERROR label?

‎src/goto-analyzer/static_simplifier.cpp

+6-6
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ bool static_simplifier(
6565

6666
if(i_it->is_assert())
6767
{
68-
exprt cond = i_it->get_condition();
68+
exprt cond = i_it->condition();
6969

7070
bool unchanged = ai.abstract_state_before(i_it)->ai_simplify(cond, ns);
7171

@@ -74,12 +74,12 @@ bool static_simplifier(
7474
else
7575
{
7676
simplified.asserts++;
77-
i_it->set_condition(cond);
77+
i_it->condition_nonconst() = cond;
7878
}
7979
}
8080
else if(i_it->is_assume())
8181
{
82-
exprt cond = i_it->get_condition();
82+
exprt cond = i_it->condition();
8383

8484
bool unchanged = ai.abstract_state_before(i_it)->ai_simplify(cond, ns);
8585

@@ -88,12 +88,12 @@ bool static_simplifier(
8888
else
8989
{
9090
simplified.assumes++;
91-
i_it->set_condition(cond);
91+
i_it->condition_nonconst() = cond;
9292
}
9393
}
9494
else if(i_it->is_goto())
9595
{
96-
exprt cond = i_it->get_condition();
96+
exprt cond = i_it->condition();
9797

9898
bool unchanged = ai.abstract_state_before(i_it)->ai_simplify(cond, ns);
9999

@@ -102,7 +102,7 @@ bool static_simplifier(
102102
else
103103
{
104104
simplified.gotos++;
105-
i_it->set_condition(cond);
105+
i_it->condition_nonconst() = cond;
106106
}
107107
}
108108
else if(i_it->is_assign())

‎src/goto-analyzer/static_verifier.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,7 @@ static_verifier_resultt::static_verifier_resultt(
115115
const namespacet &ns)
116116
{
117117
PRECONDITION(assert_location->is_assert());
118-
exprt e(assert_location->get_condition());
118+
exprt e(assert_location->condition());
119119

120120
// If there are multiple, distinct histories that reach the same location
121121
// we can get better results by checking with each individually rather

‎src/goto-analyzer/taint_analysis.cpp

+2-4
Original file line numberDiff line numberDiff line change
@@ -333,17 +333,15 @@ bool taint_analysist::operator()(
333333
if(!i_it->is_assert())
334334
continue;
335335

336-
if(!custom_bitvector_domaint::has_get_must_or_may(
337-
i_it->get_condition()))
336+
if(!custom_bitvector_domaint::has_get_must_or_may(i_it->condition()))
338337
{
339338
continue;
340339
}
341340

342341
if(custom_bitvector_analysis[i_it].has_values.is_false())
343342
continue;
344343

345-
exprt result =
346-
custom_bitvector_analysis.eval(i_it->get_condition(), i_it);
344+
exprt result = custom_bitvector_analysis.eval(i_it->condition(), i_it);
347345
if(simplify_expr(std::move(result), ns).is_true())
348346
continue;
349347

‎src/goto-instrument/accelerate/accelerate.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ goto_programt::targett acceleratet::find_back_jump(
4040
for(const auto &t : loop)
4141
{
4242
if(
43-
t->is_goto() && t->get_condition().is_true() && t->targets.size() == 1 &&
43+
t->is_goto() && t->condition().is_true() && t->targets.size() == 1 &&
4444
t->targets.front() == loop_header &&
4545
t->location_number > back_jump->location_number)
4646
{
@@ -382,7 +382,7 @@ void acceleratet::add_dirty_checks()
382382
find_symbols_sett read;
383383

384384
if(it->has_condition())
385-
find_symbols_or_nexts(it->get_condition(), read);
385+
find_symbols_or_nexts(it->condition(), read);
386386

387387
if(it->is_assign())
388388
{

‎src/goto-instrument/accelerate/acceleration_utils.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -250,7 +250,7 @@ exprt acceleration_utilst::precondition(patht &path)
250250
}
251251
else if(t->is_assume() || t->is_assert())
252252
{
253-
ret = implies_exprt(t->get_condition(), ret);
253+
ret = implies_exprt(t->condition(), ret);
254254
}
255255
else
256256
{

‎src/goto-instrument/accelerate/all_paths_enumerator.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -134,15 +134,15 @@ void all_paths_enumeratort::extend_path(
134134

135135
if(t->is_goto())
136136
{
137-
guard = not_exprt(t->get_condition());
137+
guard = not_exprt(t->condition());
138138

139139
for(goto_programt::targetst::iterator it=t->targets.begin();
140140
it != t->targets.end();
141141
++it)
142142
{
143143
if(next == *it)
144144
{
145-
guard = t->get_condition();
145+
guard = t->condition();
146146
break;
147147
}
148148
}

‎src/goto-instrument/accelerate/cone_of_influence.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ void cone_of_influencet::get_succs(
8383

8484
if(rit->is_goto())
8585
{
86-
if(!rit->get_condition().is_false())
86+
if(!rit->condition().is_false())
8787
{
8888
// Branch can be taken.
8989
for(goto_programt::targetst::const_iterator t=rit->targets.begin();
@@ -96,14 +96,14 @@ void cone_of_influencet::get_succs(
9696
}
9797
}
9898

99-
if(rit->get_condition().is_true())
99+
if(rit->condition().is_true())
100100
{
101101
return;
102102
}
103103
}
104104
else if(rit->is_assume() || rit->is_assert())
105105
{
106-
if(rit->get_condition().is_false())
106+
if(rit->condition().is_false())
107107
{
108108
return;
109109
}

‎src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -810,15 +810,15 @@ void disjunctive_polynomial_accelerationt::build_path(
810810
// If this was a conditional branch (it probably was), figure out
811811
// if we hit the "taken" or "not taken" branch & accumulate the
812812
// appropriate guard.
813-
cond = not_exprt(t->get_condition());
813+
cond = not_exprt(t->condition());
814814

815815
for(goto_programt::targetst::iterator it=t->targets.begin();
816816
it!=t->targets.end();
817817
++it)
818818
{
819819
if(next==*it)
820820
{
821-
cond = t->get_condition();
821+
cond = t->condition();
822822
break;
823823
}
824824
}

‎src/goto-instrument/accelerate/overflow_instrumenter.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ void overflow_instrumentert::add_overflow_checks(
6464
}
6565

6666
if(t->has_condition())
67-
add_overflow_checks(t, t->get_condition(), added);
67+
add_overflow_checks(t, t->condition(), added);
6868

6969
checked.insert(t->location_number);
7070
}

‎src/goto-instrument/accelerate/polynomial_accelerator.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -780,7 +780,7 @@ exprt polynomial_acceleratort::precondition(patht &path)
780780
}
781781
else if(t->is_assume() || t->is_assert())
782782
{
783-
ret = implies_exprt(t->get_condition(), ret);
783+
ret = implies_exprt(t->condition(), ret);
784784
}
785785
else
786786
{

‎src/goto-instrument/accelerate/sat_path_enumerator.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -161,15 +161,15 @@ void sat_path_enumeratort::build_path(
161161
// If this was a conditional branch (it probably was), figure out
162162
// if we hit the "taken" or "not taken" branch & accumulate the
163163
// appropriate guard.
164-
cond = not_exprt(t->get_condition());
164+
cond = not_exprt(t->condition());
165165

166166
for(goto_programt::targetst::iterator it=t->targets.begin();
167167
it!=t->targets.end();
168168
++it)
169169
{
170170
if(next==*it)
171171
{
172-
cond = t->get_condition();
172+
cond = t->condition();
173173
break;
174174
}
175175
}

0 commit comments

Comments
 (0)