1 2 #include <minix/u64.h> 3 #include <minix/minlib.h> 4 5 /* Utility function to work directly with u64_t 6 * By Antonio Mancina 7 */ 8 void read_tsc_64(t) 9 u64_t* t; 10 { 11 u32_t lo, hi; 12 read_tsc (&hi, &lo); 13 *t = make64 (lo, hi); 14 } 15 16