PARSING ERROR: syntax error before `__value' compiling with goto-cc

[stefanodallapalma]

I have the following parsing error when compiling the project https://github.com/libav/libav with goto-cc:

GEN	libavutil/libavutil.version
GEN	libswscale/libswscale.version
GEN	libavresample/libavresample.version
GEN	libavcodec/libavcodec.version
GEN	libavformat/libavformat.version
GEN	libavfilter/libavfilter.version
GEN	libavdevice/libavdevice.version
CC	libavdevice/alldevices.o
/usr/include/x86_64-linux-gnu/bits/mathcalls-helper-functions.h:21:1: error: syntax error before `__value'
PARSING ERROR
Makefile:49: recipe for target 'libavdevice/alldevices.o' failed
make: *** [libavdevice/alldevices.o] Error 1

The commands I've executed are:

1. ./configure
2. make CC=goto-cc

Compiling the project only with make works fine.

The environment I use is:
CBMC version: 5.8
goto-cc : the version contained in CBMC 5.8
Ubuntu 18.04

Any idea?

/usr/include/x86_64-linux-gnu/bits/mathcalls-helper-functions.h

/* Prototype declarations for math classification macros helpers.
   Copyright (C) 2017-2018 Free Software Foundation, Inc.
   This file is part of the GNU C Library.

   The GNU C Library is free software; you can redistribute it and/or
   modify it under the terms of the GNU Lesser General Public
   License as published by the Free Software Foundation; either
   version 2.1 of the License, or (at your option) any later version.

   The GNU C Library is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   Lesser General Public License for more details.

   You should have received a copy of the GNU Lesser General Public
   License along with the GNU C Library; if not, see
   <http://www.gnu.org/licenses/>.  */


/* Classify given number.  */
__MATHDECL_1 (int, __fpclassify,, (_Mdouble_ __value))    // <-- RAW 21
     __attribute__ ((__const__));

/* Test for negative number.  */
__MATHDECL_1 (int, __signbit,, (_Mdouble_ __value))
     __attribute__ ((__const__));

/* Return 0 if VALUE is finite or NaN, +1 if it
   is +Infinity, -1 if it is -Infinity.  */
__MATHDECL_1 (int, __isinf,, (_Mdouble_ __value)) __attribute__ ((__const__));

/* Return nonzero if VALUE is finite and not NaN.  Used by isfinite macro.  */
__MATHDECL_1 (int, __finite,, (_Mdouble_ __value)) __attribute__ ((__const__));

/* Return nonzero if VALUE is not a number.  */
__MATHDECL_1 (int, __isnan,, (_Mdouble_ __value)) __attribute__ ((__const__));

/* Test equality.  */
__MATHDECL_1 (int, __iseqsig,, (_Mdouble_ __x, _Mdouble_ __y));

/* Test for signaling NaN.  */
__MATHDECL_1 (int, __issignaling,, (_Mdouble_ __value))
     __attribute__ ((__const__));

[tautschnig]

Would you mind attaching the result of preprocessed source to this issue? The issue might be in whatever _Mdouble_ expands to. Thanks!

[stefanodallapalma]

Do you mean the result of performing goto-cc -E ?!

...
X86ASM	libavutil/x86/cpuid.o
X86ASM	libavutil/x86/emms.o
X86ASM	libavutil/x86/float_dsp.o
CC	libavutil/x86/float_dsp_init.o
X86ASM	libavutil/x86/imgutils.o
CC	libavutil/x86/imgutils_init.o
X86ASM	libavutil/x86/lls.o
CC	libavutil/x86/lls_init.o
CC	libavutil/xtea.o
AR	libavutil/libavutil.a
GEN	libavutil/libavutil.pc
CC	avtools/avconv_opt.o
CC	avtools/avconv_filter.o
CC	avtools/avconv_hw.o
CC	avtools/cmdutils.o
CC	avtools/avconv.o
LD	avconv
avtools/avconv_opt.o: file not recognized: File format not recognized
collect2: error: ld returned 1 exit status
Makefile:140: recipe for target 'avconv' failed
make: *** [avconv] Error 1

all + avconv_opt.zip

[tautschnig]

This issue will be fixed by #2146.