Closed
Description
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]
Metadata
Metadata
Assignees
Labels
No labels