OK, I am an idiot. The function I need is clock().
unsigned long timestamp = (unsigned long)((20000/7) * clock()/CLOCKS_PER_SEC);
printf("** timestamp is %lu\n", timestamp);
Maybe a better way but seems to work on Edison. Not sure why the 7 is there but CLOCKS_PER_SEC did not work. I timed it with GPS ticks.
This doesn't work. First, CLOCKS_PER_SEC is just 1000000 and that has not much to do with the clocks per second. I get about 5000 clocks per second. But it is not even. I am reading GPS inputs which are at exactly once per second. I read a large number and every 5th one reads about 7000, the rest about 4800. I can tell the difference between between 5000 and 7000 as I can tap my finger on the desk and if one was really 7000 I would expect the next one to be 3000, which it isn't, and the printf on the screen would not come out evenly like they do.
I will start a new thread.