1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 */ 10 11#ifndef __ARCH_KERNEL_THREAD_H 12#define __ARCH_KERNEL_THREAD_H 13 14#include <object.h> 15 16void Arch_switchToThread(tcb_t *tcb); 17void Arch_switchToIdleThread(void); 18void Arch_configureIdleThread(tcb_t *tcb); 19void Arch_activateIdleThread(tcb_t *tcb); 20word_t sanitiseRegister(register_t reg, word_t v, bool_t archInfo); 21 22static inline bool_t CONST 23Arch_getSanitiseRegisterInfo(tcb_t *thread) 24{ 25 return 0; 26} 27 28void Mode_postModifyRegisters(tcb_t *tptr); 29 30#endif 31