Skip to content

Commit

Permalink
Fix Alpine's assert-statement conversion special case
Browse files Browse the repository at this point in the history
In d44bfd3 we added a special case to catch Alpine Linux' assert
structure. The match, however, was not sufficiently specific as it just
accepted any statement that follows the actual assertion.

Fixes: #8436
  • Loading branch information
tautschnig committed Sep 3, 2024
1 parent 27b845c commit 26f030b
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 26f030b

Please sign in to comment.