From 4122a28b8958f6c528707bcf10a2098740b76b56 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Wed, 29 Mar 2017 16:18:08 +0100
Subject: [PATCH] Test to demonstrate assert bug on alpine

The user added assert in this test does not get coverage under alpine
linux.
---
 regression/cbmc/simple_assert/main.c    |  9 +++++++++
 regression/cbmc/simple_assert/test.desc | 13 +++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 regression/cbmc/simple_assert/main.c
 create mode 100644 regression/cbmc/simple_assert/test.desc

diff --git a/regression/cbmc/simple_assert/main.c b/regression/cbmc/simple_assert/main.c
new file mode 100644
index 00000000000..14c6fc0f682
--- /dev/null
+++ b/regression/cbmc/simple_assert/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  int x = 5;
+  assert(x == 5);
+
+  return 0;
+}
diff --git a/regression/cbmc/simple_assert/test.desc b/regression/cbmc/simple_assert/test.desc
new file mode 100644
index 00000000000..57c877afe23
--- /dev/null
+++ b/regression/cbmc/simple_assert/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.coverage\.1\] .* function main block 1: SATISFIED$
+(1 of 1|3 of 3) covered \(100\.0%\)$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+^\[main\.coverage\..\] .* function main block .: FAILED$
+--
+On Windows/Visual Studio, "assert" does not introduce any branching.