1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#pragma once 8 9#include <object.h> 10 11void Arch_switchToThread(tcb_t *tcb); 12void Arch_switchToIdleThread(void); 13void Arch_configureIdleThread(tcb_t *tcb); 14void Arch_activateIdleThread(tcb_t *tcb); 15word_t sanitiseRegister(register_t reg, word_t v, bool_t archInfo); 16 17static inline bool_t CONST Arch_getSanitiseRegisterInfo(tcb_t *thread) 18{ 19 return 0; 20} 21 22void Mode_postModifyRegisters(tcb_t *tptr); 23 24 25