int64_t is in the ICO C(C99) standard: http://www.open-std.org/jtc1/sc22/wg14/www/docs/n869/n869.pd...

Yes... as a typedef in <stdint.h>. In other words, "a userspace libc typedef" as the previous post said...

sirclueless implied that int64_t was not C99, which is wrong.

I think if you re-read what was written, what you think was implied was not.

<time.h> is userspace. It's at least theoretically possible for long long to be more than 64 bits. Why use long long (potentially, say, 128 bits) rather than int64_t for time_t?

And why wouldn't int64_t be available in kernel space?

long long can be printed in printf with the "%lld" flag.

So stdint.h not available to kernel programmers. Thanks.

I always found this special-casing of headers for kernel vs user unnecessary and complicating. In the many embedded runtimes I maintain, I've moved towards using standard POSIX-y and C(++) standard headers everywhere. I know kernel folks love to believe that their world is special so all the usual C library stuff needs to be done differently, but it's not needed.

It's so much easier to port code between the two worlds when you don't have to litter the #include prelude of every C file with conditionals.

stdint.h may not be available, but int64_t is; it's defined in include/linux/types.h.

The OpenBSD kernel probably doesn't use Linux headers.

A few times I got flamed on this site for complaining that the average HNer can't have reasonable discussions about C. I think the comment that the OpenBSD team should just #include <linux/types.h> pretty well shows that I was right. :-)

Just a silly mistake on my part.

Really going out on a limb there aren't you? ;-)

Yeah, good point.

I'm not familiar with the OpenBSD kernel. Is there any good reason (for OpenBSD or any other kernel) why <stdint.h> shouldn't be available -- or at least why int64_t shouldn't be available in some header?