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