Skip to content

Commit ace71e7

Browse files
Daniel Kroeningthk123
Daniel Kroening
authored and
thk123
committed
symex: check type consistency of assignments
1 parent 6f38516 commit ace71e7

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/goto-symex/symex_assign.cpp

+3
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,9 @@ void goto_symext::symex_assign(
2828
exprt lhs=code.lhs();
2929
exprt rhs=code.rhs();
3030

31+
DATA_INVARIANT(
32+
lhs.type() == rhs.type(), "assignments must be type consistent");
33+
3134
clean_expr(lhs, state, true);
3235
clean_expr(rhs, state, false);
3336

0 commit comments

Comments
 (0)