Skip to content

Commit cecc289

Browse files
committed
Use built-in methods
to negate boolean expression and to get address_of expression.
1 parent c7c94b2 commit cecc289

File tree

1 file changed

+2
-3
lines changed

1 file changed

+2
-3
lines changed

src/analyses/goto_check.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -1534,7 +1534,7 @@ void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard)
15341534
op.pretty());
15351535

15361536
check_rec(op, guard);
1537-
guard.add(expr.id() == ID_or ? not_exprt(op) : op);
1537+
guard.add(expr.id() == ID_or ? boolean_negate(op) : op);
15381538
}
15391539

15401540
guard = std::move(old_guard);
@@ -1641,8 +1641,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
16411641

16421642
if(expr.id()==ID_address_of)
16431643
{
1644-
assert(expr.operands().size()==1);
1645-
check_rec_address(expr.op0(), guard);
1644+
check_rec_address(to_address_of_expr(expr).object(), guard);
16461645
return;
16471646
}
16481647
else if(expr.id()==ID_and || expr.id()==ID_or)

0 commit comments

Comments
 (0)