Open
Description
CBMC version: 5.12
Operating system: Linux (Fedora Rawhide)
Exact command line resulting in the issue: make check
What behaviour did you expect: test success
What happened instead: test failure
While building version 5.12 on an x86_64 Fedora Rawhide machine with gcc 10.1.1, the test suite reported a failure:
...
Running virtual1/test.desc [FAILED]
Running windows_h_VS_2005/test.desc [OK] in 4 seconds
Running windows_h_VS_2008/test.desc [OK] in 5 seconds
Running windows_h_VS_2010/test.desc [OK] in 4 seconds
Running windows_h_VS_2012/test.desc [OK] in 4 seconds
Tests failed
1 of 96 tests failed, 3 tests skipped
Failed test: virtual1
/usr/include/bits/floatn.h:74:1: error: unexpected cpp type: complex
* #source_location:
* file: /usr/include/bits/floatn.h
* line: 74
0: floatbv
* width: 32
* f: 23
* #c_type: float
typedef _Complex float __cfloat128 __attribute__ ((__mode__ (__TC__)));
CONVERSION ERROR
EXIT=1
SIGNAL=0
Failed test.desc lines:
^EXIT=0$ [FAILED]
^CONVERSION ERROR$ [FAILED]
make[2]: Leaving directory '/builddir/build/BUILD/cbmc-cbmc-5.12/regression/cpp'
make[2]: *** [Makefile:13: test] Error 1
make[1]: *** [Makefile:64: cpp] Error 1