CBMC tests fail on Debian stable (stretch) on x86_64

[martin-cs]

This used to work. Looks like a preprocessor configuration issue. I have a /usr/include/x86_64-linux-gnu/gnu/stubs-64.h

$ make test
make[1]: Entering directory '/home/martin/working-copies/cbmc-diffblue/regression'
Running cbmc...
make -C "cbmc" test || exit 1;
make[2]: Entering directory '/home/martin/working-copies/cbmc-diffblue/regression/cbmc'
Loading
  541 tests found

Running tests
...
Tests failed
  4 of 541 tests failed, 29 tests skipped


Failed test: Pointer_Arithmetic12
CBMC version 5.9 (cbmc-5.9-404-gec79bdd62) 64-bit x86_64 linux
Parsing main.c
In file included from /usr/include/features.h:388:0,
                 from /usr/include/stdint.h:25,
                 from /usr/lib/gcc/x86_64-linux-gnu/6/include/stdint.h:9,
file                  from main.c line 1:                  from main.c:1:
file /usr/include/i386-linux-gnu/gnu/stubs.h line 10: /usr/include/i386-linux-gnu/gnu/stubs.h:10:27: fatal error: gnu/stubs-64.h: No such file or directory
 # include <gnu/stubs-64.h>
                           ^
compilation terminated.
GCC preprocessing failed
PARSING ERROR
Numeric exception : 0
EXIT=6
SIGNAL=0


Failed test.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]


Failed test: Pointer_array4
CBMC version 5.9 (cbmc-5.9-404-gec79bdd62) 64-bit x86_64 linux
Parsing main.c
In file included from /usr/include/features.h:388:0,
                 from /usr/include/assert.h:35,
file                  from main.c line 1:                  from main.c:1:
file /usr/include/i386-linux-gnu/gnu/stubs.h line 10: /usr/include/i386-linux-gnu/gnu/stubs.h:10:27: fatal error: gnu/stubs-64.h: No such file or directory
 # include <gnu/stubs-64.h>
                           ^
compilation terminated.
GCC preprocessing failed
PARSING ERROR
Numeric exception : 0
EXIT=6
SIGNAL=0


Failed test.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]


Failed test: Struct_Padding1
CBMC version 5.9 (cbmc-5.9-404-gec79bdd62) 64-bit x86_64 linux
Parsing main.c
In file included from /usr/include/features.h:388:0,
                 from /usr/include/assert.h:35,
file                  from main.c line 1:                  from main.c:1:
file /usr/include/i386-linux-gnu/gnu/stubs.h line 10: /usr/include/i386-linux-gnu/gnu/stubs.h:10:27: fatal error: gnu/stubs-64.h: No such file or directory
 # include <gnu/stubs-64.h>
                           ^
compilation terminated.
GCC preprocessing failed
PARSING ERROR
Numeric exception : 0
EXIT=6
SIGNAL=0


Failed test.desc lines:
^EXIT=0$ [FAILED]
^VERIFICATION SUCCESSFUL$ [FAILED]


Failed test: address_space_size_limit3
CBMC version 5.9 (cbmc-5.9-404-gec79bdd62) 64-bit x86_64 linux
Parsing main.c
In file included from /usr/include/features.h:388:0,
                 from /usr/include/stdint.h:25,
                 from /usr/lib/gcc/x86_64-linux-gnu/6/include/stdint.h:9,
file                  from main.c line 3:                  from main.c:3:
file /usr/include/i386-linux-gnu/gnu/stubs.h line 10: /usr/include/i386-linux-gnu/gnu/stubs.h:10:27: fatal error: gnu/stubs-64.h: No such file or directory
 # include <gnu/stubs-64.h>
                           ^
compilation terminated.
GCC preprocessing failed
PARSING ERROR
Numeric exception : 0
EXIT=6
SIGNAL=0


Failed test.desc lines:
^EXIT=10$ [FAILED]
^VERIFICATION FAILED$ [FAILED]
^.* dereference failure: pointer outside object bounds in .*: FAILURE$ [FAILED]

[martin-cs]

Release 5.9 has the same problem.

[martin-cs]

Release 5.8 works and 3 of the tests haven't been changed since then so I think it is a definite regression.

[martin-cs]

a31f530 does not have this bug
f653dec does

@kroening please can you look at this; I think your preprocessor clean-up has had some unintended side effects.

[kroening]

Does PR #2529 fix this?

[martin-cs]

I think so. develop now works so all I will close this issue.