char *s;
    if (ptr == NULL)
        s = "<unspecified>";
    else
        s = ptr;
    printf("File name: %s\n", s);