search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
843 stars 262 forks source link

aarch64: error: incompatible type for argument 1 of '__CPROVER_OBJECT_SIZE #8357

Closed vt-alt closed 1 month ago

vt-alt commented 4 months ago

CBMC version: 6.0.1 Operating system: ALT Linux Exact command line resulting in the issue: cmake --build aarch64-alt-linux --verbose --parallel 24 What behaviour did you expect: success What happened instead:

Build failure on aarch64:

[00:00:07] + cmake -DCMAKE_SKIP_INSTALL_RPATH:BOOL=yes '-DCMAKE_C_FLAGS:STRING=-pipe -frecord-gcc-switches -Wall -g -O2   -DMINISAT_CONSTANTS_AS_MACROS -Wno-error=odr' '-DCMAKE_CXX_FLAGS:STRING=-pipe -frecord-gcc-switches -Wall -g -O2   -DMINISAT_CONSTANTS_AS_MACROS -Wno-error=odr' '-DCMAKE_Fortran_FLAGS:STRING=-pipe -frecord-gcc-switches -Wall -g -O2   -DMINISAT_CONSTANTS_AS_MACROS -Wno-error=odr' -DCMAKE_INSTALL_PREFIX=/usr -DINCLUDE_INSTALL_DIR:PATH=/usr/include -DLIB_INSTALL_DIR:PATH=/usr/lib64 -DSYSCONF_INSTALL_DIR:PATH=/etc -DSHARE_INSTALL_PREFIX:PATH=/usr/share -DLIB_DESTINATION=lib64 -DLIB_SUFFIX=64 -S . -B aarch64-alt-linux -DWITH_JBMC:BOOL=OFF -DBUILD_SHARED_LIBS:BOOL=OFF -Dsat_impl=system-cadical
[00:00:08] + cmake --build aarch64-alt-linux --verbose --parallel 24
...
[00:02:11] [ 42%] Generating library-check.stamp
[00:02:11] cd /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c && /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library_check.sh /usr/bin/cc /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/cegis.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/cprover_contracts.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/ctype.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/err.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/errno.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/fcntl.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/fenv.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/float.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/gcc.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/getopt.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/inet.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/intrin.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/locale.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/math.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/mman.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/netdb.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/process.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/pthread_lib.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/pwd.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/random.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/semaphore.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/setjmp.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/signal.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/stdio.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/stdlib.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/string.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/strings.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/syslog.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/time.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/unistd.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/windows.c /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/x86_assembler.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/cegis.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/cprover_contracts.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/ctype.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/err.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/errno.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/fcntl.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/fenv.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/float.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/gcc.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/getopt.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/inet.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/intrin.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/locale.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/math.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/mman.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/netdb.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/process.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/pthread_lib.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/pwd.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/random.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/semaphore.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/setjmp.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/signal.c
[00:02:11] Checking /usr/src/RPM/BUILD/cbmc-6.0.1/src/ansi-c/library/stdio.c
[00:02:11] __libcheck.c: In function 'vsnprintf':
[00:02:11] __libcheck.c:1777:31: error: incompatible type for argument 1 of '__CPROVER_OBJECT_SIZE'
[00:02:11]  1777 |         __CPROVER_OBJECT_SIZE(ap))
[00:02:11]       |                               ^~
[00:02:11]       |                               |
[00:02:11]       |                               va_list
[00:02:11] In file included from ./library/cprover.h:75,
[00:02:11]                  from <command-line>:
[00:02:11] ./library/../cprover_builtin_headers.h:59:40: note: expected 'const void *' but argument is of type 'va_list'
[00:02:11]    59 | __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
[00:02:11]       |                                        ^~~~~~~~~~~~
[00:02:11] __libcheck.c:1782:65: error: incompatible type for argument 1 of '__CPROVER_POINTER_OBJECT'
[00:02:11]  1782 |       __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
[00:02:11]       |                                                                 ^~
[00:02:11]       |                                                                 |
[00:02:11]       |                                                                 va_list
[00:02:11] ./library/../cprover_builtin_headers.h:57:43: note: expected 'const void *' but argument is of type 'va_list'
[00:02:11]    57 | __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
[00:02:11]       |                                           ^~~~~~~~~~~~
[00:02:11] __libcheck.c: In function 's__builtin___vsnprintf_chk':
[00:02:11] __libcheck.c:1825:31: error: incompatible type for argument 1 of '__CPROVER_OBJECT_SIZE'
[00:02:11]  1825 |         __CPROVER_OBJECT_SIZE(ap))
[00:02:11]       |                               ^~
[00:02:11]       |                               |
[00:02:11]       |                               va_list
[00:02:11] ./library/../cprover_builtin_headers.h:59:40: note: expected 'const void *' but argument is of type 'va_list'
[00:02:11]    59 | __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
[00:02:11]       |                                        ^~~~~~~~~~~~
[00:02:11] __libcheck.c:1830:65: error: incompatible type for argument 1 of '__CPROVER_POINTER_OBJECT'
[00:02:11]  1830 |       __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
[00:02:11]       |                                                                 ^~
[00:02:11]       |                                                                 |
[00:02:11]       |                                                                 va_list
[00:02:11] ./library/../cprover_builtin_headers.h:57:43: note: expected 'const void *' but argument is of type 'va_list'
[00:02:11]    57 | __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
[00:02:11]       |                                           ^~~~~~~~~~~~
[00:02:11] At top level:
[00:02:11] cc1: note: unrecognized command-line option '-Wno-unknown-warning-option' may have been intended to silence earlier diagnostics
[00:02:11] cc1: note: unrecognized command-line option '-Wno-gnu-line-marker' may have been intended to silence earlier diagnostics
[00:02:11] cc1: note: unrecognized command-line option '-Wno-dollar-in-identifier-extension' may have been intended to silence earlier diagnostics
[00:02:11] rm: cannot remove '__libcheck.s': No such file or directory
[00:02:11] gmake[2]: *** [src/ansi-c/CMakeFiles/ansi-c.dir/build.make:293: src/ansi-c/library-check.stamp] Error 1
[00:02:11] gmake[2]: Leaving directory '/usr/src/RPM/BUILD/cbmc-6.0.1/aarch64-alt-linux'
[00:02:11] gmake[1]: *** [CMakeFiles/Makefile2:1966: src/ansi-c/CMakeFiles/ansi-c.dir/all] Error 2
[00:02:11] gmake: *** [Makefile:166: all] Error 2

Noting that there was similar issue in 2023: https://github.com/diffblue/cbmc/issues/7862

lzaoral commented 3 months ago

With #8366 applied, I still get following errors on aarch64 Fedora Rawhide and CBMC 6.0.1:

Checking /builddir/build/BUILD/cbmc-6.0.1-build/cbmc-cbmc-6.0.1/src/ansi-c/library/stdio.c
__libcheck.c: In function ‘vsnprintf’:
__libcheck.c:1782:65: error: incompatible type for argument 1 of ‘__CPROVER_POINTER_OBJECT’
 1782 |       __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
      |                                                                 ^~
      |                                                                 |
      |                                                                 va_list
In file included from ./library/cprover.h:75,
                 from <command-line>:
./library/../cprover_builtin_headers.h:57:43: note: expected ‘const void *’ but argument is of type ‘va_list’
   57 | __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
      |                                           ^~~~~~~~~~~~
__libcheck.c: In function ‘s__builtin___vsnprintf_chk’:
__libcheck.c:1830:65: error: incompatible type for argument 1 of ‘__CPROVER_POINTER_OBJECT’
 1830 |       __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
      |                                                                 ^~
      |                                                                 |
      |                                                                 va_list
./library/../cprover_builtin_headers.h:57:43: note: expected ‘const void *’ but argument is of type ‘va_list’
   57 | __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
      |                                           ^~~~~~~~~~~~
At top level:
cc1: note: unrecognized command-line option ‘-Wno-unknown-warning-option’ may have been intended to silence earlier diagnostics
cc1: note: unrecognized command-line option ‘-Wno-gnu-line-marker’ may have been intended to silence earlier diagnostics
cc1: note: unrecognized command-line option ‘-Wno-dollar-in-identifier-extension’ may have been intended to silence earlier diagnostics
rm: cannot remove '__libcheck.s': No such file or directory