Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
vt-alt opened this issue Jun 22, 2024 · 1 comment · Fixed by #8366
Closed

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

vt-alt opened this issue Jun 22, 2024 · 1 comment · Fixed by #8366
Labels
pending merge

Comments

@vt-alt
Copy link

vt-alt commented Jun 22, 2024

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: #7862
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jul 2, 2024
@tautschnig
fixup! C model library: Support ARM64 va_list types
20e7cef 
This extends 4d0164f to uses within `__CPROVER_OBJECT_SIZE`.

Fixes: diffblue#8357
@tautschnig tautschnig mentioned this issue Jul 2, 2024
Merged
3 tasks
@lzaoral
Copy link
Contributor

lzaoral commented Jul 18, 2024

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

tautschnig added a commit to tautschnig/kani that referenced this issue Aug 9, 2024
@tautschnig
Update CBMC build instructions for Amazon Linux 2
b60b9c6 
The default compiler on Amazon Linux 2 is GCC 7, which is not
sufficiently recent for building CBMC v6+. Install and use GCC 10,
adjust warnings to cope with the flex version provided by Amazon Linux
2, and handle the non-default std::filesystem support. Furthermore,
apply a workaround until diffblue/cbmc#8357
has been fixed on the CBMC side.
@tautschnig tautschnig mentioned this issue Aug 9, 2024
Merged
github-merge-queue bot pushed a commit to model-checking/kani that referenced this issue Aug 9, 2024
@tautschnig
Update CBMC build instructions for Amazon Linux 2 (#3431)
bec5fd1 
The default compiler on Amazon Linux 2 is GCC 7, which is not
sufficiently recent for building CBMC v6+. Install and use GCC 10,
adjust warnings to cope with the flex version provided by Amazon Linux
2, and handle the non-default std::filesystem support. Furthermore,
apply a workaround until diffblue/cbmc#8357
has been fixed on the CBMC side.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
pending merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

C library: fix use of va_list for AARCH64 tautschnig/cbmc
3 participants
@tautschnig @vt-alt @lzaoral