Wrong result using __va_list_tag_type with multiple arguments

[evgeny7421]

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

[tautschnig]

Thank you for this test! It seems that 35cc503 will require some additional work to catch the case you demonstrate.