Skip to content

Commit

Permalink
Check havoc does not encounter unsupported expressions
Browse files Browse the repository at this point in the history
In order to ensure failure rather than unsound analysis in this case.
  • Loading branch information
thomasspriggs committed Jul 27, 2023
1 parent 815a9a2 commit b8e01ac
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion src/goto-symex/symex_other.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,11 @@ void goto_symext::havoc_rec(
}
else
{
// consider printing a warning
INVARIANT_WITH_DIAGNOSTICS(
false,
"Attempted to symex havoc applied to unsupported expression",
state.source.pc->code().pretty(),
dest.pretty());
}
}

Expand Down

0 comments on commit b8e01ac

Please sign in to comment.