Skip to content

Commit

Permalink
Merge pull request diffblue#8438 from tautschnig/fix-8436-conversion
Browse files Browse the repository at this point in the history
Fix Alpine's assert-statement conversion special case
  • Loading branch information
tautschnig committed Sep 5, 2024
2 parents 71ee177 + 4b5fae8 commit d67648a
Show file tree
Hide file tree
Showing 3 changed files with 33 additions and 1 deletion.
22 changes: 22 additions & 0 deletions regression/ansi-c/goto_convert_assert/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
void __assert_fail(char *, char *, unsigned, char *);

int main()
{
(void)((1 < 2) || (__CPROVER_assert(0, ""), 0));

int jumpguard;
jumpguard = (jumpguard | 1);
label_1:;
{
while(1)
{
if(jumpguard == 0)
{
__assert_fail("0", "lc2.c", 8U, "func");
goto label_1;
}
goto label_2;
}
label_2:;
}
}
7 changes: 7 additions & 0 deletions regression/ansi-c/goto_convert_assert/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE test-c++-front-end
main.c

^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
5 changes: 4 additions & 1 deletion src/ansi-c/goto-conversion/goto_convert.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1812,8 +1812,11 @@ void goto_convertt::generate_ifthenelse(
if(
is_empty(false_case) && true_case.instructions.size() == 2 &&
true_case.instructions.front().is_assert() &&
true_case.instructions.front().condition().is_false() &&
simplify_expr(true_case.instructions.front().condition(), ns).is_false() &&
true_case.instructions.front().labels.empty() &&
true_case.instructions.back().is_other() &&
true_case.instructions.back().get_other().get_statement() ==
ID_expression &&
true_case.instructions.back().labels.empty())
{
true_case.instructions.front().condition_nonconst() = boolean_negate(guard);
Expand Down

0 comments on commit d67648a

Please sign in to comment.