Skip to content

Compilation error on ARM64 Linux #7862

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
adpaco-aws opened this issue Aug 23, 2023 · 1 comment · Fixed by #7863
Closed

Compilation error on ARM64 Linux #7862

adpaco-aws opened this issue Aug 23, 2023 · 1 comment · Fixed by #7863

Comments

@adpaco-aws
Copy link
Contributor

CBMC version: 5.90.0 (tag: cbmc-5.90.0)
Operating system: Ubuntu 22.04
Exact command line resulting in the issue: make -C build -j$(nproc) after cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
What behaviour did you expect: Compilation finishes successfully.
What happened instead: Compilation fails with:

Checking /home/ubuntu/cbmc/src/ansi-c/library/stdio.c
__libcheck.c: In function '__isoc99_vfscanf':
__libcheck.c:1050:31: error: incompatible type for argument 1 of '__CPROVER_OBJECT_SIZE'
 1050 |         __CPROVER_OBJECT_SIZE(arg))
      |                               ^~~
      |                               |
      |                               va_list
In file included from ./library/cprover.h:72,
                 from <command-line>:
./library/../cprover_builtin_headers.h:59:40: note: expected 'const void *' but argument is of type 'va_list'
   59 | __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
      |                                        ^~~~~~~~~~~~
__libcheck.c: In function '__isoc99_vsscanf':
__libcheck.c:1213:31: error: incompatible type for argument 1 of '__CPROVER_OBJECT_SIZE'
 1213 |         __CPROVER_OBJECT_SIZE(arg))
      |                               ^~~
      |                               |
      |                               va_list
In file included from ./library/cprover.h:72,
                 from <command-line>:
./library/../cprover_builtin_headers.h:59:40: note: expected 'const void *' but argument is of type 'va_list'
   59 | __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
      |                                        ^~~~~~~~~~~~
__libcheck.c: 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
rm: cannot remove '__libcheck.s': No such file or directory
make[2]: *** [src/ansi-c/CMakeFiles/ansi-c.dir/build.make:279: src/ansi-c/library-check.stamp] Error 1
make[2]: Leaving directory '/home/ubuntu/cbmc/build'
make[1]: *** [CMakeFiles/Makefile2:2075: src/ansi-c/CMakeFiles/ansi-c.dir/all] Error 2
make[1]: Leaving directory '/home/ubuntu/cbmc/build'
make: *** [Makefile:166: all] Error 2
make: Leaving directory '/home/ubuntu/cbmc/build'
@adpaco-aws
Copy link
Contributor Author

Noting here that this issue is similar to #7423

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant