From dab6a6e18a80ebded3ce348b55b966cf35fc6a07 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 6 Jul 2018 18:56:18 +0100 Subject: [PATCH] Fix tests that are only correct on little-endian architectures --- regression/cbmc/byte_update2/test.desc | 2 +- regression/cbmc/byte_update3/test.desc | 2 +- regression/cbmc/byte_update4/test.desc | 2 +- regression/cbmc/byte_update5/test.desc | 2 +- regression/cbmc/byte_update6/test.desc | 2 +- regression/cbmc/byte_update7/test.desc | 2 +- regression/cbmc/byte_update8/test.desc | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/regression/cbmc/byte_update2/test.desc b/regression/cbmc/byte_update2/test.desc index 9efefbc7362..9845e70d84b 100644 --- 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 index 9efefbc7362..9845e70d84b 100644 --- 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 index 9efefbc7362..9845e70d84b 100644 --- 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 index 9efefbc7362..9845e70d84b 100644 --- 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 index 9efefbc7362..9845e70d84b 100644 --- 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 index 9efefbc7362..9845e70d84b 100644 --- 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 index 9efefbc7362..9845e70d84b 100644 --- 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$