From 4b5fae83287d442fdc75a86d95450622ca6f69ac Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 3 Sep 2024 17:50:27 +0000
Subject: [PATCH] Fix Alpine's assert-statement conversion special case

In d44bfd3a1545b 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
---
 regression/ansi-c/goto_convert_assert/main.c  | 22 +++++++++++++++++++
 .../ansi-c/goto_convert_assert/test.desc      |  7 ++++++
 src/ansi-c/goto-conversion/goto_convert.cpp   |  5 ++++-
 3 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100644 regression/ansi-c/goto_convert_assert/main.c
 create mode 100644 regression/ansi-c/goto_convert_assert/test.desc

diff --git a/regression/ansi-c/goto_convert_assert/main.c b/regression/ansi-c/goto_convert_assert/main.c
new file mode 100644
index 00000000000..8fe327ae3aa
--- /dev/null
+++ b/regression/ansi-c/goto_convert_assert/main.c
@@ -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:;
+  }
+}
diff --git a/regression/ansi-c/goto_convert_assert/test.desc b/regression/ansi-c/goto_convert_assert/test.desc
new file mode 100644
index 00000000000..68779b2b0e3
--- /dev/null
+++ b/regression/ansi-c/goto_convert_assert/test.desc
@@ -0,0 +1,7 @@
+CORE test-c++-front-end
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp
index 793fba651c3..f07ed0f424c 100644
--- a/src/ansi-c/goto-conversion/goto_convert.cpp
+++ b/src/ansi-c/goto-conversion/goto_convert.cpp
@@ -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);