Closed
Description
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