Skip to content

Commit 6e2c03e

Browse files
author
Daniel Kroening
committed
symex: check type consistency of assignments
1 parent 3ff9bbe commit 6e2c03e

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/goto-symex/symex_assign.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,8 @@ void goto_symext::symex_assign(
2828
exprt lhs=code.lhs();
2929
exprt rhs=code.rhs();
3030

31+
DATA_INVARIANT(lhs.type() == rhs.type(), "assignments must be type consistent");
32+
3133
clean_expr(lhs, state, true);
3234
clean_expr(rhs, state, false);
3335

0 commit comments

Comments
 (0)