Skip to content

Commit 3179414

Browse files
tautschnigtautschnig
committed
Use operator==(exprt, bool)
Replaces uses of `is_true` and `is_false`.
1 parent fba2cce commit 3179414

File tree

110 files changed

+279
-280
lines changed

Some content is hidden

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

110 files changed

+279
-280
lines changed

‎jbmc/src/java_bytecode/expr2java.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -179,9 +179,9 @@ std::string expr2javat::convert_constant(
179179
}
180180
else if(src.is_boolean())
181181
{
182-
if(src.is_true())
182+
if(src == true)
183183
return "true";
184-
else if(src.is_false())
184+
else if(src == false)
185185
return "false";
186186
}
187187
else if(src.type().id()==ID_pointer)

‎jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1087,7 +1087,7 @@ void java_object_factoryt::gen_nondet_init(
10871087
else
10881088
{
10891089
exprt within_bounds = interval.make_contains_expr(expr);
1090-
if(!within_bounds.is_true())
1090+
if(within_bounds != true)
10911091
assignments.add(code_assumet(std::move(within_bounds)));
10921092
}
10931093

‎jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ static bool is_call_to(
6969

7070
static bool is_assume_false(goto_programt::const_targett inst)
7171
{
72-
return inst->is_assume() && inst->condition().is_false();
72+
return inst->is_assume() && inst->condition() == false;
7373
}
7474

7575
/// Interpret `program`, resolving classid comparisons assuming any actual
@@ -90,12 +90,12 @@ static goto_programt::const_targett interpret_classid_comparison(
9090
{
9191
exprt guard = pc->condition();
9292
guard = resolve_classid_test(guard, actual_class_id, ns);
93-
if(guard.is_true())
93+
if(guard == true)
9494
{
9595
REQUIRE(pc->targets.begin() != pc->targets.end());
9696
pc = *(pc->targets.begin());
9797
}
98-
else if(guard.is_false())
98+
else if(guard == false)
9999
++pc;
100100
else
101101
{

‎src/analyses/constant_propagator.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -183,8 +183,8 @@ void constant_propagator_domaint::transform(
183183
else
184184
g = not_exprt(from->condition());
185185
partial_evaluate(values, g, ns);
186-
if(g.is_false())
187-
values.set_to_bottom();
186+
if(g == false)
187+
values.set_to_bottom();
188188
else
189189
two_way_propagate_rec(g, ns, cp);
190190
}
@@ -376,7 +376,7 @@ bool constant_propagator_domaint::two_way_propagate_rec(
376376

377377
// x != FALSE ==> x == TRUE
378378

379-
if(rhs.is_zero() || rhs.is_false())
379+
if(rhs == 0 || rhs == false)
380380
rhs = from_integer(1, rhs.type());
381381
else
382382
rhs = from_integer(0, rhs.type());

‎src/analyses/custom_bitvector_analysis.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -530,7 +530,7 @@ void custom_bitvector_domaint::transform(
530530

531531
const exprt result2 = simplify_expr(eval(guard, cba), ns);
532532

533-
if(result2.is_false())
533+
if(result2 == false)
534534
make_bottom();
535535
}
536536
break;
@@ -814,9 +814,9 @@ void custom_bitvector_analysist::check(
814814
if(use_xml)
815815
{
816816
out << "<result status=\"";
817-
if(result.is_true())
817+
if(result == true)
818818
out << "SUCCESS";
819-
else if(result.is_false())
819+
else if(result == false)
820820
out << "FAILURE";
821821
else
822822
out << "UNKNOWN";
@@ -838,9 +838,9 @@ void custom_bitvector_analysist::check(
838838
out << '\n';
839839
}
840840

841-
if(result.is_true())
841+
if(result == true)
842842
pass++;
843-
else if(result.is_false())
843+
else if(result == false)
844844
fail++;
845845
else
846846
unknown++;

‎src/analyses/goto_rw.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -116,9 +116,9 @@ void rw_range_sett::get_objects_if(
116116
const range_spect &range_start,
117117
const range_spect &size)
118118
{
119-
if(if_expr.cond().is_false())
119+
if(if_expr.cond() == false)
120120
get_objects_rec(mode, if_expr.false_case(), range_start, size);
121-
else if(if_expr.cond().is_true())
121+
else if(if_expr.cond() == true)
122122
get_objects_rec(mode, if_expr.true_case(), range_start, size);
123123
else
124124
{
@@ -735,9 +735,9 @@ void rw_guarded_range_set_value_sett::get_objects_if(
735735
const range_spect &range_start,
736736
const range_spect &size)
737737
{
738-
if(if_expr.cond().is_false())
738+
if(if_expr.cond() == false)
739739
get_objects_rec(mode, if_expr.false_case(), range_start, size);
740-
else if(if_expr.cond().is_true())
740+
else if(if_expr.cond() == true)
741741
get_objects_rec(mode, if_expr.true_case(), range_start, size);
742742
else
743743
{

‎src/analyses/guard_bdd.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ exprt guard_bddt::guard_expr(exprt expr) const
4444
}
4545
else
4646
{
47-
if(expr.is_false())
47+
if(expr == false)
4848
{
4949
return boolean_negate(as_expr());
5050
}

‎src/analyses/guard_expr.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ exprt guard_exprt::guard_expr(exprt expr) const
2424
}
2525
else
2626
{
27-
if(expr.is_false())
27+
if(expr == false)
2828
{
2929
return boolean_negate(as_expr());
3030
}
@@ -39,9 +39,9 @@ void guard_exprt::add(const exprt &expr)
3939
{
4040
PRECONDITION(expr.is_boolean());
4141

42-
if(is_false() || expr.is_true())
42+
if(is_false() || expr == true)
4343
return;
44-
else if(is_true() || expr.is_false())
44+
else if(is_true() || expr == false)
4545
{
4646
this->expr = expr;
4747

@@ -198,7 +198,7 @@ guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2)
198198

199199
if(tmp != and_expr1)
200200
{
201-
if(and_expr1.is_true() || and_expr2.is_true())
201+
if(and_expr1 == true || and_expr2 == true)
202202
{
203203
}
204204
else

‎src/analyses/guard_expr.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_ANALYSES_GUARD_EXPR_H
1313
#define CPROVER_ANALYSES_GUARD_EXPR_H
1414

15-
#include <util/expr.h>
15+
#include <util/std_expr.h>
1616

1717
/// This is unused by this implementation of guards, but can be used by other
1818
/// implementations of the same interface.
@@ -59,12 +59,12 @@ class guard_exprt
5959

6060
bool is_true() const
6161
{
62-
return expr.is_true();
62+
return expr == true;
6363
}
6464

6565
bool is_false() const
6666
{
67-
return expr.is_false();
67+
return expr == false;
6868
}
6969

7070
friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2);

‎src/analyses/interval_analysis.cpp

Lines changed: 2 additions & 2 deletions
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->condition().is_true())
49+
if(previous->is_goto() && previous->condition() != true)
5050
{
5151
// we follow a branch, instrument
5252
}
@@ -69,7 +69,7 @@ void instrument_intervals(
6969
for(const auto &symbol_expr : symbols)
7070
{
7171
exprt tmp=d.make_expression(symbol_expr);
72-
if(!tmp.is_true())
72+
if(tmp != true)
7373
assertion.push_back(tmp);
7474
}
7575

‎src/analyses/interval_domain.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -501,7 +501,7 @@ bool interval_domaint::ai_simplify(
501501
// of when condition is true
502502
if(!a.join(d)) // If d (this) is included in a...
503503
{ // Then the condition is always true
504-
unchanged=condition.is_true();
504+
unchanged=condition == true;
505505
condition = true_exprt();
506506
}
507507
}
@@ -514,7 +514,7 @@ bool interval_domaint::ai_simplify(
514514
d.assume(not_exprt(condition), ns); // Restrict to when condition is false
515515
if(d.is_bottom()) // If there there are none...
516516
{ // Then the condition is always true
517-
unchanged=condition.is_true();
517+
unchanged=condition == true;
518518
condition = true_exprt();
519519
}
520520
}

‎src/analyses/invariant_set.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -394,11 +394,11 @@ void invariant_sett::strengthen_rec(const exprt &expr)
394394
return;
395395
}
396396

397-
if(expr.is_true())
397+
if(expr == true)
398398
{
399399
// do nothing, it's useless
400400
}
401-
else if(expr.is_false())
401+
else if(expr == false)
402402
{
403403
// wow, that's strong
404404
make_false();
@@ -596,7 +596,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
596596
if(is_false) // can't get any stronger
597597
return tvt(true);
598598

599-
if(expr.is_true())
599+
if(expr == true)
600600
return tvt(true);
601601
else if(expr.id()==ID_not)
602602
{
@@ -701,12 +701,12 @@ void invariant_sett::nnf(exprt &expr, bool negate)
701701
if(!expr.is_boolean())
702702
throw "nnf: non-Boolean expression";
703703

704-
if(expr.is_true())
704+
if(expr == true)
705705
{
706706
if(negate)
707707
expr=false_exprt();
708708
}
709-
else if(expr.is_false())
709+
else if(expr == false)
710710
{
711711
if(negate)
712712
expr=true_exprt();

‎src/analyses/local_cfg.cpp

Lines changed: 1 addition & 1 deletion
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.condition().is_true())
38+
if(instruction.condition() != true)
3939
node.successors.push_back(loc_nr+1);
4040

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

‎src/analyses/variable-sensitivity/abstract_environment.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -275,7 +275,7 @@ bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)
275275
// Should be of the right type
276276
INVARIANT(assumption.is_boolean(), "simplification preserves type");
277277

278-
if(assumption.is_false())
278+
if(assumption == false)
279279
{
280280
bool currently_bottom = is_bottom();
281281
make_bottom();
@@ -582,7 +582,7 @@ static exprt invert_result(const exprt &result)
582582
if(!result.is_boolean())
583583
return result;
584584

585-
if(result.is_true())
585+
if(result == true)
586586
return false_exprt();
587587
return true_exprt();
588588
}
@@ -640,7 +640,7 @@ exprt assume_and(
640640
for(auto const &operand : and_expr.operands())
641641
{
642642
auto result = env.do_assume(operand, ns);
643-
if(result.is_false())
643+
if(result == false)
644644
return result;
645645
nil |= result.is_nil();
646646
}
@@ -833,7 +833,7 @@ exprt assume_less_than(
833833
auto reduced_le_expr =
834834
binary_relation_exprt(left_lower, expr.id(), right_upper);
835835
auto result = env.eval(reduced_le_expr, ns)->to_constant();
836-
if(result.is_true())
836+
if(result == true)
837837
{
838838
if(is_assignable(operands.lhs))
839839
{

‎src/analyses/variable-sensitivity/abstract_value_object.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -664,8 +664,8 @@ class value_set_evaluator
664664
for(const auto &v : condition)
665665
{
666666
auto expr = v->to_constant();
667-
all_true = all_true && expr.is_true();
668-
all_false = all_false && expr.is_false();
667+
all_true = all_true && expr == true;
668+
all_false = all_false && expr == false;
669669
}
670670
auto indeterminate = !all_true && !all_false;
671671

‎src/analyses/variable-sensitivity/full_array_abstract_object.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -426,7 +426,7 @@ exprt full_array_abstract_objectt::to_predicate_internal(
426426
auto index = index_exprt(name, ii);
427427
auto field_expr = field.second->to_predicate(index);
428428

429-
if(!field_expr.is_true())
429+
if(field_expr != true)
430430
all_predicates.push_back(field_expr);
431431
}
432432

‎src/analyses/variable-sensitivity/full_struct_abstract_object.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -312,7 +312,7 @@ exprt full_struct_abstract_objectt::to_predicate_internal(
312312
member_exprt(name, compound_type.get_component(field.first));
313313
auto field_expr = field.second->to_predicate(field_name);
314314

315-
if(!field_expr.is_true())
315+
if(field_expr != true)
316316
all_predicates.push_back(field_expr);
317317
}
318318

‎src/analyses/variable-sensitivity/interval_abstract_value.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -45,8 +45,7 @@ class interval_index_ranget : public index_range_implementationt
4545
{
4646
index = next;
4747
next = next_element(next, ns);
48-
return simplify_expr(binary_predicate_exprt(index, ID_le, upper), ns)
49-
.is_true();
48+
return simplify_expr(binary_predicate_exprt(index, ID_le, upper), ns) == true;
5049
}
5150

5251
index_range_implementation_ptrt reset() const override
@@ -239,7 +238,7 @@ bool new_interval_is_top(const constant_interval_exprt &e)
239238
if(e.is_top())
240239
return true;
241240

242-
if(e.get_lower().is_false() && e.get_upper().is_true())
241+
if(e.get_lower() == false && e.get_upper() == true)
243242
return true;
244243
if(
245244
e.type().id() == ID_c_bool && e.get_lower().is_zero() &&

‎src/analyses/variable-sensitivity/value_set_abstract_object.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -441,11 +441,11 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
441441
set,
442442
[](const abstract_value_objectt &value) {
443443
auto c = value.to_constant();
444-
return c.is_false() || (c.id() == ID_min_value);
444+
return c == false || (c.id() == ID_min_value);
445445
},
446446
[](const abstract_value_objectt &value) {
447447
auto c = value.to_constant();
448-
return c.is_true() || (c.id() == ID_max_value);
448+
return c == true || (c.id() == ID_max_value);
449449
});
450450
}
451451

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,7 @@ void c_typecheck_baset::typecheck_code(codet &code)
116116
implicit_typecast_bool(code.op0());
117117
make_constant(code.op0());
118118

119-
if(code.op0().is_false())
119+
if(code.op0() == false)
120120
{
121121
// failed
122122
error().source_location = code.find_source_location();
@@ -951,7 +951,7 @@ void c_typecheck_baset::typecheck_conditional_targets(
951951
auto &condition = conditional_target_group.condition();
952952
typecheck_spec_condition(condition);
953953

954-
if(condition.is_true())
954+
if(condition == true)
955955
{
956956
// if the condition is trivially true,
957957
// simplify expr and expose the bare expressions

0 commit comments

Comments
 (0)