Open
Description
CBMC version: cbmc-5.82.0
Operating system: CentOS Linux release 7.7.1908 (Core)
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: passing assertions
What happened instead: crash
If I just replace __va_list_tag_type with __builtin_va_list, it works
main.c, modified your own regression test
#ifdef __GNUC__
# include <assert.h>
typedef typeof(((__builtin_va_list*)0)[0][0]) __va_list_tag_type;
void my_f(int first, ...)
{
__va_list_tag_type args[1];
__builtin_va_start(args, first);
int v;
v=__builtin_va_arg(args, int);
assert(v==1);
v=__builtin_va_arg(args, int);
assert(v==0);
__builtin_va_end(args);
}
int main()
{
my_f(2, 1, 0);
}
#else
// __builtin_va_list is GCC/Clang-only
int main()
{
}
#endif