After update to version 5.5 some tests started to fail on big endian arches (ppc64, s390x) from build.log ... Tests failed 2 of 383 tests failed, 19 tests skipped Failed test: Pointer_array5 CBMC version 5.5 64-bit s390x linux Parsing main.c file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined <built-in>: note: this is the location of the previous definition Converting Type-checking main Generating GOTO Program Adding CPROVER library (s390x) file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined <built-in>: note: this is the location of the previous 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.042s ** Results: [main.assertion.1] assertion address==&a0: FAILURE ** 1 of 1 failed (1 iteration) VERIFICATION FAILED EXIT=10 SIGNAL=0 Failed test: Pointer_byte_extract5 CBMC version 5.5 64-bit s390x linux Parsing main.c file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined <built-in>: note: this is the location of the previous definition Converting Type-checking main Generating GOTO Program Adding CPROVER library (s390x) file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined <built-in>: note: this is the location of the previous definition Removal of function pointers and virtual functions Partial Inlining Generic Property Instrumentation Starting Bounded Model Checking size of program expression: 73 steps simple slicing removed 5 assignments Generated 9 VCC(s), 9 remaining after simplification Passing problem to propositional reduction converting SSA Running propositional reduction Post-processing Solving with MiniSAT 2.2.1 with simplifier 302 variables, 54 clauses SAT checker: instance is SATISFIABLE Solving with MiniSAT 2.2.1 with simplifier 302 variables, 1 clauses SAT checker: instance is SATISFIABLE Solving with MiniSAT 2.2.1 with simplifier 302 variables, 0 clauses SAT checker inconsistent: instance is UNSATISFIABLE Runtime decision procedure: 0.003s ** Results: [main.array_bounds.1] array.List upper bound in p->List[0]: SUCCESS [main.array_bounds.2] array.List upper bound in p->List[0]: SUCCESS [main.assertion.1] p->List[0].b==555: SUCCESS [main.assertion.2] p->List[0].a==555: SUCCESS [main.array_bounds.3] array.List upper bound in p->List[1]: SUCCESS [main.array_bounds.4] array.List upper bound in p->List[1]: SUCCESS [main.assertion.3] p->List[1].b==999: FAILURE [main.assertion.4] p->List[1].a==999: FAILURE [main.array_bounds.5] array.List upper bound in p->List[2]: FAILURE ** 3 of 9 failed (3 iterations) VERIFICATION FAILED EXIT=10 SIGNAL=0 Makefile:4: recipe for target 'test' failed make[1]: Leaving directory '/builddir/build/BUILD/cbmc-src/regression/cbmc' make[1]: *** [test] Error 1 Makefile:4: recipe for target 'test' failed make: Leaving directory '/builddir/build/BUILD/cbmc-src/regression' make: *** [test] Error 1 .. for full logs please see http://s390.koji.fedoraproject.org/koji/taskinfo?taskID=2332684 or http://ppc.koji.fedoraproject.org/koji/taskinfo?taskID=3658891 Version-Release number of selected component (if applicable): cbmc-5.5-1.fc26
I don't have access to any big endian machines. I've had guest accounts on various people's machines in the past. I ran through all of them this morning, and all of the machines are either inaccessible or don't recognize my former username + password. If somebody can provide me with an account on some big endian hardware somewhere, I am quite happy to debug this issue. Anybody? Anbody? Bueller? Just eyeballing the two failing tests, my guess is that the Pointer_array5 failure might go away if -fno-strict-aliasing is used. The Pointer_byte_extract5 failure is more puzzling. The first failing assertion happens like this: p->List[1].b = 999; __CPROVER_assert(p->List[1].b==999, "p->List[1].b==999"); We set that value to 999, then assert that the value is 999, and it isn't. But the array index is higher than the array size declared by the packed type. So I'm going to go out on a limb and conjecture that using a flexible array in the type declaration will fix this one; i.e., patching the code so the #ifdef __GNUC__ case reads: typedef struct { int Count; Union List[]; } __attribute__((packed)) Struct3; If nobody is able to give me an account somewhere, could one of you with access to hardware please add this to %prep and try building again? # Fix a test with type aliasing sed -i '/main\.c/a-fno-strict-aliasing' regression/cbmc/Pointer_array5/test.desc # Fix a test with out-of-bounds access to a packed array sed -i '/__GNUC__/,/else/s/List\[1\]/List[]/' regression/cbmc/Pointer_byte_extract5/main.c
(In reply to Jerry James from comment #1) > I don't have access to any big endian machines. I've had guest accounts on > various people's machines in the past. I ran through all of them this > morning, and all of the machines are either inaccessible or don't recognize > my former username + password. If somebody can provide me with an account > on some big endian hardware somewhere, I am quite happy to debug this issue. > Anybody? Anbody? Bueller? > please take a look at following link to get access to th s390x machine http://www-03.ibm.com/systems/z/os/linux/support/community.html > Just eyeballing the two failing tests, my guess is that the Pointer_array5 > failure might go away if -fno-strict-aliasing is used. The > Pointer_byte_extract5 failure is more puzzling. The first failing assertion > happens like this: > > p->List[1].b = 999; > > __CPROVER_assert(p->List[1].b==999, "p->List[1].b==999"); > > We set that value to 999, then assert that the value is 999, and it isn't. > But the array index is higher than the array size declared by the packed > type. So I'm going to go out on a limb and conjecture that using a flexible > array in the type declaration will fix this one; i.e., patching the code so > the #ifdef __GNUC__ case reads: > > typedef struct > { > int Count; > Union List[]; > } __attribute__((packed)) Struct3; > > If nobody is able to give me an account somewhere, could one of you with > access to hardware please add this to %prep and try building again? > > # Fix a test with type aliasing > sed -i '/main\.c/a-fno-strict-aliasing' > regression/cbmc/Pointer_array5/test.desc > cbmc doesn't support this flag and failed with: * * CBMC 5.5 - Copyright (C) 2001-2016 (64-bit version) * * * * Daniel Kroening, Edmund Clarke * * * * Carnegie Mellon University, Computer Science Department * * * * kroening * * * * Protected in part by U.S. patent 7,225,417 * * Usage: Purpose: cbmc [-?] [-h] [--help] show help cbmc file.c ... source file names .. > # Fix a test with out-of-bounds access to a packed array > sed -i '/__GNUC__/,/else/s/List\[1\]/List[]/' > regression/cbmc/Pointer_byte_extract5/main.c comfirmed that it fixes the issue
trace for the failed properties CBMC version 5.5 64-bit s390x linux Parsing regression/cbmc/Pointer_array5/main.c file <Kommandozeile> line 0: <Kommandozeile>:0:0: Warnung: »__STDC_VERSION__« redefiniert file <eingebaut> line 0: <eingebaut>:0:0: Anmerkung: dies ist die Stelle der vorherigen Definition Converting Type-checking main Generating GOTO Program Adding CPROVER library (s390x) file <Kommandozeile> line 0: <Kommandozeile>:0:0: Warnung: »__STDC_VERSION__« redefiniert file <eingebaut> line 0: <eingebaut>: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
cbmc-5.5-2.fc25 has been submitted as an update to Fedora 25. https://bodhi.fedoraproject.org/updates/FEDORA-2016-886bd77454
cbmc-5.5-2.fc24 has been submitted as an update to Fedora 24. https://bodhi.fedoraproject.org/updates/FEDORA-2016-d045b1594c
cbmc-5.5-2.fc24 has been pushed to the Fedora 24 testing repository. If problems still persist, please make note of it in this bug report. See https://fedoraproject.org/wiki/QA:Updates_Testing for instructions on how to install test updates. You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2016-d045b1594c
cbmc-5.5-2.fc25 has been pushed to the Fedora 25 testing repository. If problems still persist, please make note of it in this bug report. See https://fedoraproject.org/wiki/QA:Updates_Testing for instructions on how to install test updates. You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2016-886bd77454
cbmc-5.5-2.fc25 has been pushed to the Fedora 25 stable repository. If problems still persist, please make note of it in this bug report.
cbmc-5.5-2.fc24 has been pushed to the Fedora 24 stable repository. If problems still persist, please make note of it in this bug report.