Skip to content

Commit e546b83

Browse files
committed
Check havoc does not encounter unsupported expressions
In order to ensure failure rather than unsound analysis in this case.
1 parent 0130d37 commit e546b83

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

src/goto-symex/symex_other.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,11 @@ void goto_symext::havoc_rec(
6868
}
6969
else
7070
{
71-
// consider printing a warning
71+
INVARIANT_WITH_DIAGNOSTICS(
72+
false,
73+
"Attempted to symex havoc applied to unsupported expression",
74+
state.source.pc->code().pretty(),
75+
dest.pretty());
7276
}
7377
}
7478

0 commit comments

Comments
 (0)