POK
|
00001 /* 00002 * POK header 00003 * 00004 * The following file is a part of the POK project. Any modification should 00005 * made according to the POK licence. You CANNOT use this file or a part of 00006 * this file is this part of a file for your own project 00007 * 00008 * For more information on the POK licence, please see our LICENCE FILE 00009 * 00010 * Please follow the coding guidelines described in doc/CODING_GUIDELINES 00011 * 00012 * Copyright (c) 2007-2009 POK team 00013 * 00014 * Created by julien on Thu Jan 15 23:34:13 2009 00015 */ 00016 00017 00018 #ifdef POK_NEEDS_ARINC653_TIME 00019 00020 #include <arinc653/types.h> 00021 #include <arinc653/time.h> 00022 00023 #include <core/thread.h> 00024 #include <types.h> 00025 00026 00027 #ifndef POK_CONFIG_OPTIMIZE_FOR_GENERATED_CODE 00028 void TIMED_WAIT (SYSTEM_TIME_TYPE delay_time, RETURN_CODE_TYPE *return_code) 00029 { 00030 (void) delay_time; 00031 *return_code = NOT_AVAILABLE; 00032 } 00033 #endif 00034 00035 void PERIODIC_WAIT (RETURN_CODE_TYPE *return_code) 00036 { 00037 pok_ret_t core_ret; 00038 core_ret = pok_thread_period (); 00039 *return_code = core_ret; 00040 } 00041 00042 #ifndef POK_CONFIG_OPTIMIZE_FOR_GENERATED_CODE 00043 void GET_TIME (SYSTEM_TIME_TYPE *system_time, RETURN_CODE_TYPE *return_code) 00044 { 00045 (void) system_time; 00046 *return_code = NOT_AVAILABLE; 00047 } 00048 00049 void REPLENISH (SYSTEM_TIME_TYPE budget_time, RETURN_CODE_TYPE *return_code) 00050 { 00051 (void) budget_time; 00052 *return_code = NOT_AVAILABLE; 00053 } 00054 #endif 00055 00056 #endif 00057