Skip to content

Commit 13e2eca

Browse files
committed
use divisor()/dividend() methods
This commit replaces uses of .op0() and .op1() by accessor methods specific to division operators.
1 parent 4085b97 commit 13e2eca

File tree

2 files changed

+9
-9
lines changed

2 files changed

+9
-9
lines changed

src/ansi-c/goto_check_c.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -618,8 +618,8 @@ void goto_check_ct::mod_by_zero_check(
618618

619619
// add divison by zero subgoal
620620

621-
exprt zero = from_integer(0, expr.op1().type());
622-
const notequal_exprt inequality(expr.op1(), std::move(zero));
621+
exprt zero = from_integer(0, expr.divisor().type());
622+
const notequal_exprt inequality(expr.divisor(), std::move(zero));
623623

624624
add_guarded_property(
625625
inequality,

src/solvers/flattening/boolbv_mod.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -25,25 +25,25 @@ bvt boolbvt::convert_mod(const mod_exprt &expr)
2525
std::size_t width=boolbv_width(expr.type());
2626

2727
DATA_INVARIANT(
28-
expr.op0().type().id() == expr.type().id(),
29-
"type of the first operand of a modulo operation shall equal the "
28+
expr.dividend().type().id() == expr.type().id(),
29+
"type of the dividend of a modulo operation shall equal the "
3030
"expression type");
3131

3232
DATA_INVARIANT(
33-
expr.op1().type().id() == expr.type().id(),
34-
"type of the second operand of a modulo operation shall equal the "
33+
expr.divisor().type().id() == expr.type().id(),
34+
"type of the divisor of a modulo operation shall equal the "
3535
"expression type");
3636

3737
bv_utilst::representationt rep=
3838
expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
3939
bv_utilst::representationt::UNSIGNED;
4040

41-
const bvt &op0 = convert_bv(expr.op0(), width);
42-
const bvt &op1 = convert_bv(expr.op1(), width);
41+
const bvt &dividend_bv = convert_bv(expr.dividend(), width);
42+
const bvt &divisor_bv = convert_bv(expr.divisor(), width);
4343

4444
bvt res, rem;
4545

46-
bv_utils.divider(op0, op1, res, rem, rep);
46+
bv_utils.divider(dividend_bv, divisor_bv, res, rem, rep);
4747

4848
return rem;
4949
}

0 commit comments

Comments
 (0)