tests fail on big endian arches (s390x/ppc64)

[ngothan]

CBMC version 5.5 64-bit s390x linux
Parsing regression/cbmc/Pointer_array5/main.c
file line 0: :0:0: Warnung: »STDC_VERSION« redefiniert
file line 0: :0:0: Anmerkung: dies ist die Stelle der vorherigen Definition
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (s390x)
file line 0: :0:0: Warnung: »STDC_VERSION« redefiniert
file line 0: :0:0: Anmerkung: dies ist die Stelle der vorherigen Definition
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 95 steps
simple slicing removed 24 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
12568 variables, 25409 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.038s

** Results:
[main.assertion.1] assertion address==&a0: FAILURE

Trace for main.assertion.1:

State 18 file regression/cbmc/Pointer_array5/main.c line 8 function main thread 0

arraylen=0 (00000000000000000000000000000000)

State 19 file regression/cbmc/Pointer_array5/main.c line 8 function main thread 0

arraylen=3 (00000000000000000000000000000011)

State 21 file regression/cbmc/Pointer_array5/main.c line 12 function main thread 0

array_init=((signed int **)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 41 file regression/cbmc/Pointer_array5/main.c line 12 function main thread 0

array_init=dynamic_object1 (0000001000000000000000000000000000000000000000000000000000000000)

State 42 file regression/cbmc/Pointer_array5/main.c line 14 function main thread 0

a0=0 (00000000000000000000000000000000)

State 43 file regression/cbmc/Pointer_array5/main.c line 14 function main thread 0

a1=0 (00000000000000000000000000000000)

State 44 file regression/cbmc/Pointer_array5/main.c line 14 function main thread 0

a2=0 (00000000000000000000000000000000)

State 45 file regression/cbmc/Pointer_array5/main.c line 16 function main thread 0

dynamic_object1[0l]=&a0!0@1 (0000001100000000000000000000000000000000000000000000000000000000)

State 46 file regression/cbmc/Pointer_array5/main.c line 17 function main thread 0

dynamic_object1[1l]=&a1!0@1 (0000010000000000000000000000000000000000000000000000000000000000)

State 47 file regression/cbmc/Pointer_array5/main.c line 18 function main thread 0

dynamic_object1[2l]=&a2!0@1 (0000010100000000000000000000000000000000000000000000000000000000)

State 48 file regression/cbmc/Pointer_array5/main.c line 20 function main thread 0

local_array=((const void **)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 49 file regression/cbmc/Pointer_array5/main.c line 20 function main thread 0

local_array=dynamic_object1 (0000001000000000000000000000000000000000000000000000000000000000)

State 50 file regression/cbmc/Pointer_array5/main.c line 22 function main thread 0

address=((signed int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 51 file regression/cbmc/Pointer_array5/main.c line 22 function main thread 0

address=((signed int *)NULL) + 192 (0000000000000000000000000000000000000000000000000000000011000000)

Violated property:
file regression/cbmc/Pointer_array5/main.c line 23 function main
assertion address==&a0
address == &a0

** 1 of 1 failed (1 iteration)
VERIFICATION FAILED

[tautschnig]

Closing as the bugs in byte-extract operations have been fixed (some time before releasing 5.10, the Debian package of which no longer disabled the regression test mentioned in this issue; 5.6 still had that test disabled).