Skip to content

Commit d67648a

Browse files
authored
Merge pull request #8438 from tautschnig/fix-8436-conversion
Fix Alpine's assert-statement conversion special case
2 parents 71ee177 + 4b5fae8 commit d67648a

File tree

3 files changed

+33
-1
lines changed

3 files changed

+33
-1
lines changed

Diff for: regression/ansi-c/goto_convert_assert/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void __assert_fail(char *, char *, unsigned, char *);
2+
3+
int main()
4+
{
5+
(void)((1 < 2) || (__CPROVER_assert(0, ""), 0));
6+
7+
int jumpguard;
8+
jumpguard = (jumpguard | 1);
9+
label_1:;
10+
{
11+
while(1)
12+
{
13+
if(jumpguard == 0)
14+
{
15+
__assert_fail("0", "lc2.c", 8U, "func");
16+
goto label_1;
17+
}
18+
goto label_2;
19+
}
20+
label_2:;
21+
}
22+
}

Diff for: regression/ansi-c/goto_convert_assert/test.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE test-c++-front-end
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring

Diff for: src/ansi-c/goto-conversion/goto_convert.cpp

+4-1
Original file line numberDiff line numberDiff line change
@@ -1812,8 +1812,11 @@ void goto_convertt::generate_ifthenelse(
18121812
if(
18131813
is_empty(false_case) && true_case.instructions.size() == 2 &&
18141814
true_case.instructions.front().is_assert() &&
1815-
true_case.instructions.front().condition().is_false() &&
1815+
simplify_expr(true_case.instructions.front().condition(), ns).is_false() &&
18161816
true_case.instructions.front().labels.empty() &&
1817+
true_case.instructions.back().is_other() &&
1818+
true_case.instructions.back().get_other().get_statement() ==
1819+
ID_expression &&
18171820
true_case.instructions.back().labels.empty())
18181821
{
18191822
true_case.instructions.front().condition_nonconst() = boolean_negate(guard);

0 commit comments

Comments
 (0)