Loop invariants cause va_list to fail

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

For the following program:

int my_f(int x, ...)
{
  __builtin_va_list list;
  __builtin_va_start(list, x);

  int value;
  unsigned i;

  for(i=0; i<x; i++)
  __CPROVER_loop_invariant (
     list == __CPROVER_loop_entry(list) + i && (value == 10 || i == 0)
  )
  {
    value=__builtin_va_arg(list, int);
  }
  return value;
}

int main()
{
  assert(my_f(1, 10)==10);
}

CBMC fails to prove that the invariant preserves.

I suppose the cause of failure is that __builtin_va_arg(p, int) is statically rewritten to va_args[j] where va_args is the build-in array of arguments. However, after havocing, p becomes a nondet pointer; hence __builtin_va_arg(p, int) cannot be correctly rewritten (and will be rewritten to symex::invalid_object!0#0 as an example).
To resolve the issue, we could rewrite __builtin_va_arg(p, int) to

1. check if p is the same object as va_args: assert(same_object(p,va_args))
2. check if the offset of p is valid: assert(offset(p) < object_size(va_args))
3. substitute __builtin_va_arg(p, int) with (int)(*p)

[qinheping]

Cannot reproduce the failure now. The issue does not persists. I suppose it is fixed by #6326.