All versions of varargs.h and/or stdarg.h I've seen either define va_end as an empty macro or some opaque compiler-specific function that I guess doesn't do anything either. The rationale in the C standard states "some implementations might need it", but gives no more details.
When would there be a real need for a va_end()? Any examples of ABI that would require such, preferably with an explanation?
C has been around for a long, long time and has many standards. These standards tend to give compilers some leeway, letting them implement their own padding/headers/etc. for performance and other reasons. I assume this was added because, as mentioned, "some compilers might need it." Though languages try to abstract their implementation details, some things - inevitably - slip through the cracks... Hope this was helpful =]
