Merge pull request diffblue#2530 from tautschnig/debian3

Fix tests that are only correct on little-endian architectures
NathanJPhillips · Jul 7, 2018 · 425db26 · 425db26
2 parents 0da9766 + dab6a6e
commit 425db26
Show file tree

Hide file tree

Showing 7 changed files with 7 additions and 7 deletions.
diff --git a/regression/cbmc/byte_update2/test.desc b/regression/cbmc/byte_update2/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--little-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

diff --git a/regression/cbmc/byte_update3/test.desc b/regression/cbmc/byte_update3/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--little-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

diff --git a/regression/cbmc/byte_update4/test.desc b/regression/cbmc/byte_update4/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--little-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

diff --git a/regression/cbmc/byte_update5/test.desc b/regression/cbmc/byte_update5/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--little-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

diff --git a/regression/cbmc/byte_update6/test.desc b/regression/cbmc/byte_update6/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--little-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

diff --git a/regression/cbmc/byte_update7/test.desc b/regression/cbmc/byte_update7/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--little-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

diff --git a/regression/cbmc/byte_update8/test.desc b/regression/cbmc/byte_update8/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--little-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$