The transformation of va_arg is broken on 64-bit linux. The problem seems to be that __builtin_va_arg is prototyped with arguments (va_list, uint) in cil.ml but this should be (va_list, ulong). The problem manifests itself when
va_arg(ap, int) is transformed to
__builtin_va_arg(ap, (unsigned int) sizeof(int)) which is no longer matched by the pattern in cabs2cil.ml (the pattern is "marker :: SizeOf resType :: _".
The fix may be simply to change the prototype to take ulong, although a more robust fix may be to prevent CIL from doing any transformations to the code after va_arg is parsed into the SizeOf() form.