PARSING ERROR syntax error before '__value' when verifying hardware of DUAL_PATH_ADDER of the FM16 paper's benchmark.

[Shawn-Yang-Xiao]

I encounter following error when trying hw-cbmc on the benchmarks of DUAL_PATH_ADDER (which is in http://www.cs.ox.ac.uk/people/rajdeep.mukherjee/FM16-experiments.tar.gz).

HW-CBMC version 5.94.0 (cbmc-5.94.0-dirty)
Starting Bounded Model Checking
Parsing fp_comparison.c
file /usr/include/x86_64-linux-gnu/bits/mathcalls-helper-functions.h line 20: syntax error before '__value'
PARSING ERROR

the command is

time ~/hw-cbmc/src/hw-cbmc/hw-cbmc fp_comparison.c fp_adder.v --module fp_add_sub --bound 1 hw_cbmc_harness.c

This error report seems to be similar to #2152 if cbmc, but I use new version of cbmc and hw-cbmc.

I am using Ubuntu 22.04, and

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

/* Prototype declarations for math classification macros helpers.
   Copyright (C) 2017-2022 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
   <https://www.gnu.org/licenses/>.  */

/* Classify given number.  */
__MATHDECL_ALIAS (int, __fpclassify,, (_Mdouble_ __value), fpclassify)
     __attribute__ ((__const__));

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

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

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

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

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

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

[tautschnig]

It seems that hw-cbmc will also need a fix akin to diffblue/cbmc@9c4d2dfc8f6033c35815e67113ec20257ee42723.

[lee-man]

any solution? @Shawn-Yang-Xiao