Skip to content

Compilation error on aarch64-linux #7423

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.

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

Closed
jiegec opened this issue Dec 9, 2022 · 1 comment · Fixed by #7521
Closed

Compilation error on aarch64-linux #7423

jiegec opened this issue Dec 9, 2022 · 1 comment · Fixed by #7521

Comments

@jiegec
Copy link

jiegec commented Dec 9, 2022

CBMC version: 5.72.1 (commit de504f5)
Operating system: Ubuntu 22.04
Exact command line resulting in the issue: make
What behaviour did you expect: It should compile
What happened instead: Compilation fails

Commands:

$ cmake .. -DWITH_JBMC=OFF -Dsat_impl=cadical
$ make
Checking /home/jiegec/nixpkgs-dev/cbmc/src/ansi-c/library/stdio.c
__libcheck.c: In function ‘vfscanf’:
__libcheck.c:986:52: error: incompatible type for argument 1 of ‘__CPROVER_POINTER_OFFSET’
  986 |   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
      |                                                    ^~~
      |                                                    |
      |                                                    va_list
In file included from ./library/cprover.h:43,
                 from <command-line>:
./library/../cprover_builtin_headers.h:62:44: note: expected ‘const void *’ but argument is of type ‘va_list’
   62 | __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
      |                                            ^~~~~~~~~~~~
__libcheck.c:987:31: error: incompatible type for argument 1 of ‘__CPROVER_OBJECT_SIZE’
  987 |         __CPROVER_OBJECT_SIZE(arg))
      |                               ^~~
      |                               |
      |                               va_list
In file included from ./library/cprover.h:43,
                 from <command-line>:
./library/../cprover_builtin_headers.h:63:40: note: expected ‘const void *’ but argument is of type ‘va_list’
   63 | __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
      |                                        ^~~~~~~~~~~~
__libcheck.c: In function ‘__isoc99_vfscanf’:
__libcheck.c:1033:52: error: incompatible type for argument 1 of ‘__CPROVER_POINTER_OFFSET’
 1033 |   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
      |                                                    ^~~
      |                                                    |
      |                                                    va_list
In file included from ./library/cprover.h:43,
                 from <command-line>:
./library/../cprover_builtin_headers.h:62:44: note: expected ‘const void *’ but argument is of type ‘va_list’
   62 | __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
      |                                            ^~~~~~~~~~~~
__libcheck.c:1034:31: error: incompatible type for argument 1 of ‘__CPROVER_OBJECT_SIZE’
 1034 |         __CPROVER_OBJECT_SIZE(arg))
      |                               ^~~
      |                               |
      |                               va_list
In file included from ./library/cprover.h:43,
                 from <command-line>:
./library/../cprover_builtin_headers.h:63:40: note: expected ‘const void *’ but argument is of type ‘va_list’
   63 | __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
      |                                        ^~~~~~~~~~~~
__libcheck.c: In function ‘vsscanf’:
__libcheck.c:1155:52: error: incompatible type for argument 1 of ‘__CPROVER_POINTER_OFFSET’
 1155 |   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
      |                                                    ^~~
      |                                                    |
      |                                                    va_list
In file included from ./library/cprover.h:43,
                 from <command-line>:
./library/../cprover_builtin_headers.h:62:44: note: expected ‘const void *’ but argument is of type ‘va_list’
   62 | __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
      |                                            ^~~~~~~~~~~~
__libcheck.c:1156:31: error: incompatible type for argument 1 of ‘__CPROVER_OBJECT_SIZE’
 1156 |         __CPROVER_OBJECT_SIZE(arg))
      |                               ^~~
      |                               |
      |                               va_list
In file included from ./library/cprover.h:43,
                 from <command-line>:
./library/../cprover_builtin_headers.h:63:40: note: expected ‘const void *’ but argument is of type ‘va_list’
   63 | __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
      |                                        ^~~~~~~~~~~~
__libcheck.c: In function ‘__isoc99_vsscanf’:
__libcheck.c:1188:52: error: incompatible type for argument 1 of ‘__CPROVER_POINTER_OFFSET’
 1188 |   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
      |                                                    ^~~
      |                                                    |
      |                                                    va_list
In file included from ./library/cprover.h:43,
                 from <command-line>:
./library/../cprover_builtin_headers.h:62:44: note: expected ‘const void *’ but argument is of type ‘va_list’
   62 | __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
      |                                            ^~~~~~~~~~~~
__libcheck.c:1189:31: error: incompatible type for argument 1 of ‘__CPROVER_OBJECT_SIZE’
 1189 |         __CPROVER_OBJECT_SIZE(arg))
      |                               ^~~
      |                               |
      |                               va_list
In file included from ./library/cprover.h:43,
                 from <command-line>:
./library/../cprover_builtin_headers.h:63:40: note: expected ‘const void *’ but argument is of type ‘va_list’
   63 | __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
      |                                        ^~~~~~~~~~~~
rm: cannot remove '__libcheck.s': No such file or directory
make[2]: *** [src/ansi-c/CMakeFiles/ansi-c.dir/build.make:267: src/ansi-c/library-check.stamp] Error 1
make[1]: *** [CMakeFiles/Makefile2:1858: src/ansi-c/CMakeFiles/ansi-c.dir/all] Error 2
make: *** [Makefile:166: all] Error 2
@jiegec
Copy link
Author

jiegec commented Dec 9, 2022

The offending commit is d0e7f39(#7369) via bisecting. @tautschnig

@tautschnig tautschnig self-assigned this Jan 12, 2023
tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 4, 2023
GCC/ARM appears to uses a struct to represent variadic arguments (where
the first component is a pointer to the stack of arguments). Taking the
pointer offset requires looking at the first element of this struct,
which we do by taking the address, casting to a pointer, and
dereferencing.

Fixes: diffblue#7423
@tautschnig tautschnig removed their assignment Feb 4, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants