18 #ifdef POK_NEEDS_ARINC653_TIME
22 #include <arinc653/types.h>
42 extern void TIMED_WAIT (
43 SYSTEM_TIME_TYPE delay_time,
44 RETURN_CODE_TYPE *return_code );
46 extern void PERIODIC_WAIT (
47 RETURN_CODE_TYPE *return_code );
49 extern void GET_TIME (
50 SYSTEM_TIME_TYPE *system_time,
51 RETURN_CODE_TYPE *return_code );
53 void REPLENISH (SYSTEM_TIME_TYPE budget_time, RETURN_CODE_TYPE *return_code);