asctime - day of month zero or space padded?

I have the following program demonstrating the use of asctime.

#include <stdio.h>
#include <time.h>

int main(void) {
    struct tm   broken_down;
    broken_down.tm_year = 2000 - 1900;
    broken_down.tm_mon = 0;
    broken_down.tm_mday = 1;
    broken_down.tm_hour = broken_down.tm_min = broken_down.tm_sec = 0;

    printf("Current date and time: %s", asctime(&broken_down));
}

This program prints Current date and time: Sun Jan 1 00:00:00 2000, on ideone.com, i.e. the date field is space-padded.

When I compile and run this program with MSVC it produces the date string with leading zero on the day of month: Current date and time: Sun Jan 01 00:00:00 2000.

What is the reason for this discrepancy? Which format is correct?

As usual, the authors of Microsoft's (non-)standard C library have not given much thought to implementing the letter of standard correctly.

Even in the original standard C89/C90 the following text appears

Description

The asctime function converts the broken-down time in the structure pointed to by timeptr into a string in the form

Sun Sep 16 01:03:52 1973\n\0

using the equivalent of the following algorithm.

char *asctime(const struct tm *timeptr)
{
    static const char wday_name[7][3] = {
             "Sun", "Mon", "Tue", "Wed", "Thu", "Fri", "Sat"
    };
    static const char mon_name[12][3] = {
             "Jan", "Feb", "Mar", "Apr", "May", "Jun",
             "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"
    };
    static char result[26];

    sprintf(result, "%.3s %.3s%3d %.2d:%.2d:%.2d %d\n",
             wday_name[timeptr->tm_wday],
             mon_name[timeptr->tm_mon],
             timeptr->tm_mday, timeptr->tm_hour,
             timeptr->tm_min, timeptr->tm_sec,
             1900 + timeptr->tm_year);
    return result;
}

The example itself unfortunately uses a date that has a 2-digit day of month, but the code clearly uses %3d which means a decimal number without leading zeroes space-padded and right-justified within a 3-character-wide field.

The result for the given broken-down time is Sun Jan 1 00:00:00 2000 with space-padding.

Python 2, ever until 2.7.15 has been exposing the C standard library asctime output as-is, less the newline, which has caused platform-dependent behaviour. It was fixed in 2.7.15 to use a hard-coded format with leading space. The Python 2 documentation, too, uses a date with 2-digit day of month in its example, adding to further confusion.