From 26803f7ee4998a3632ea64b343acc22dced2605b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Sat, 7 Jul 2018 06:35:31 +0100
Subject: [PATCH] Test only works with simplification enabled

... and simplification is only performed for byte_extract_little_endian.
---
 regression/cbmc/scanf1/big-endian.desc    |  8 ++++++++
 regression/cbmc/scanf1/{main.c => main.i} | 19 ++++++++-----------
 regression/cbmc/scanf1/no-simplify.desc   |  8 ++++++++
 regression/cbmc/scanf1/test.desc          |  4 ++--
 4 files changed, 26 insertions(+), 13 deletions(-)
 create mode 100644 regression/cbmc/scanf1/big-endian.desc
 rename regression/cbmc/scanf1/{main.c => main.i} (57%)
 create mode 100644 regression/cbmc/scanf1/no-simplify.desc

diff --git a/regression/cbmc/scanf1/big-endian.desc b/regression/cbmc/scanf1/big-endian.desc
new file mode 100644
index 00000000000..6a4549ce627
--- /dev/null
+++ b/regression/cbmc/scanf1/big-endian.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.i
+--big-endian
+^EXIT=10$
+^SIGNAL=0$
+^\*\* 8 of 8 failed
+--
+^warning: ignoring
diff --git a/regression/cbmc/scanf1/main.c b/regression/cbmc/scanf1/main.i
similarity index 57%
rename from regression/cbmc/scanf1/main.c
rename to regression/cbmc/scanf1/main.i
index 55ca6a4af5f..960ceda8498 100644
--- a/regression/cbmc/scanf1/main.c
+++ b/regression/cbmc/scanf1/main.i
@@ -1,6 +1,3 @@
-#include <stdio.h>
-#include <assert.h>
-
 int main(void)
 {
   char c=0;
@@ -23,14 +20,14 @@ int main(void)
   __CPROVER_scanf("%p", &p);
   __CPROVER_scanf("%s", buffer);
 
-  assert(c==0); // may fail
-  assert(si==0); // may fail
-  assert(i==0); // may fail
-  assert(f==0); // may fail
-  assert(d==0); // may fail
-  assert(li==0); // may fail
-  assert(p==0); // may fail
-  assert(buffer[0]==0); // may fail
+  __CPROVER_assert(c == 0, "may fail");
+  __CPROVER_assert(si == 0, "may fail");
+  __CPROVER_assert(i == 0, "may fail");
+  __CPROVER_assert(f == 0, "may fail");
+  __CPROVER_assert(d == 0, "may fail");
+  __CPROVER_assert(li == 0, "may fail");
+  __CPROVER_assert(p == 0, "may fail");
+  __CPROVER_assert(buffer[0] == 0, "may fail");
 
   return 0;
 }
diff --git a/regression/cbmc/scanf1/no-simplify.desc b/regression/cbmc/scanf1/no-simplify.desc
new file mode 100644
index 00000000000..d2cc73330b1
--- /dev/null
+++ b/regression/cbmc/scanf1/no-simplify.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.i
+--little-endian --no-simplify
+^EXIT=10$
+^SIGNAL=0$
+^\*\* 8 of 8 failed
+--
+^warning: ignoring
diff --git a/regression/cbmc/scanf1/test.desc b/regression/cbmc/scanf1/test.desc
index b20bfc6b36a..346519020ae 100644
--- a/regression/cbmc/scanf1/test.desc
+++ b/regression/cbmc/scanf1/test.desc
@@ -1,6 +1,6 @@
 CORE
-main.c
-
+main.i
+--little-endian
 ^EXIT=10$
 ^SIGNAL=0$
 ^\*\* 8 of 8 failed