Source: cbmc Version: 5.95.1-4 Severity: serious Tags: ftbfs Hi Maintainer
As can be seen in reproducible builds [1], cbmc FTBFS on arm64 with glibc 2.38. I've copied what I hope is the relevant part of the log below. A bug was filed against glibc [2], but it seems glibc upstream do not consider it a bug in glibc. Regards Graham [1] https://tests.reproducible-builds.org/debian/rb-pkg/cbmc.html [2] https://sourceware.org/bugzilla/show_bug.cgi?id=30909 [31mTests failed [0m 10 of 1114 tests failed, 60 tests skipped Failed test: Float-div2 CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux Parsing main.c file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax error before '__f32x4_t' PARSING ERROR EXIT=6 SIGNAL=0 Failed test.desc lines: ^EXIT=0$ [FAILED] ^VERIFICATION SUCCESSFUL$ [FAILED] Failed test: Float-div3 CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux Parsing main.c file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax error before '__f32x4_t' PARSING ERROR EXIT=6 SIGNAL=0 Failed test.desc lines: ^EXIT=0$ [FAILED] ^VERIFICATION SUCCESSFUL$ [FAILED] Failed test: Float-equality2 CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux Parsing main.c file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax error before '__f32x4_t' PARSING ERROR EXIT=6 SIGNAL=0 Failed test.desc lines: (Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$) [FAILED] ^VERIFICATION SUCCESSFUL$ [FAILED] ^EXIT=0$ [FAILED] Failed test: Float-flags-no-simp1 CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux Parsing main.c file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax error before '__f32x4_t' PARSING ERROR EXIT=6 SIGNAL=0 Failed test.desc lines: ^EXIT=0$ [FAILED] ^VERIFICATION SUCCESSFUL$ [FAILED] Failed test: Float-flags-simp1 CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux Parsing main.c file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax error before '__f32x4_t' PARSING ERROR EXIT=6 SIGNAL=0 Failed test.desc lines: ^EXIT=0$ [FAILED] ^VERIFICATION SUCCESSFUL$ [FAILED] Failed test: Float-no-simp9 CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux Parsing main.c file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax error before '__f32x4_t' PARSING ERROR EXIT=6 SIGNAL=0 Failed test.desc lines: ^EXIT=0$ [FAILED] ^VERIFICATION SUCCESSFUL$ [FAILED] Failed test: Float21 CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux Parsing main.c file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax error before '__f32x4_t' PARSING ERROR EXIT=6 SIGNAL=0 Failed test.desc lines: ^EXIT=0$ [FAILED] ^VERIFICATION SUCCESSFUL$ [FAILED] Failed test: float-nan-check CBMC version 5.95.1 (cbmc-5.95.1) 64-bit arm64 linux Parsing main.c file /usr/include/aarch64-linux-gnu/bits/math-vector.h line 30: syntax error before '__f32x4_t' PARSING ERROR EXIT=6 SIGNAL=0
