L4Re - L4 Runtime Environment
1 /*
2  * (c) 2009 Adam Lackorzynski <adam@os.inf.tu-dresden.de>,
3  * Alexander Warg <warg@os.inf.tu-dresden.de>
4  * economic rights: Technische Universit├Ąt Dresden (Germany)
5  *
6  * This file is part of TUD:OS and distributed under the terms of the
7  * GNU General Public License 2.
8  * Please see the COPYING-GPL-2 file for details.
9  *
10  * As a special exception, you may use this file as part of a free software
11  * library without restriction. Specifically, if other files instantiate
12  * templates or use macros or inline functions from this file, or you compile
13  * this file and link it with other files to produce an executable, this
14  * file does not by itself cause the resulting executable to be covered by
15  * the GNU General Public License. This exception does not however
16  * invalidate any other reasons why the executable file might be covered by
17  * the GNU General Public License.
18  */
19 #pragma once
21 #include <l4/sys/types.h>
22 #include <l4/sys/__vcpu-arch.h>
47 typedef struct l4_vcpu_state_t
48 {
49  l4_umword_t version;
50  l4_umword_t user_data[7];
57  l4_uint16_t _reserved;
63  l4_umword_t reserved_sp;
64  l4_vcpu_arch_state_t arch_state;
72 {
73  L4_VCPU_F_IRQ = 0x01,
79 };
86 {
88 };
95 {
98 };
111 L4_INLINE int
112 l4_vcpu_check_version(l4_vcpu_state_t const *vcpu) L4_NOTHROW;
114 /* IMPLEMENTATION: ------------------------------------------------*/
116 L4_INLINE int
117 l4_vcpu_check_version(l4_vcpu_state_t const *vcpu) L4_NOTHROW
118 {
119  return vcpu->version == L4_VCPU_STATE_VERSION;
120 }
State of a vCPU.
Definition: vcpu.h:47
Offset where extended state begins.
Definition: vcpu.h:96
unsigned short int l4_uint16_t
Unsigned 16bit value.
Definition: l4int.h:38
Common L4 ABI Data Types.
l4_vcpu_ipc_regs_t i
IPC state.
Definition: vcpu.h:52
struct l4_vcpu_state_t l4_vcpu_state_t
State of a vCPU.
Sticky flags of a vCPU.
Definition: vcpu.h:85
unsigned long l4_cap_idx_t
L4 Capability selector Type.
Definition: types.h:342
Offset where extended infos begin.
Definition: vcpu.h:97
User task will be used.
Definition: vcpu.h:77
FPU enabled.
Definition: vcpu.h:78
Page faults enabled.
Definition: vcpu.h:74
Offsets for vCPU state layouts.
Definition: vcpu.h:94
Exception enabled.
Definition: vcpu.h:75
unsigned long l4_umword_t
Unsigned machine word.
Definition: l4int.h:52
l4_umword_t entry_sp
Stack pointer for entry (when coming from user task)
Definition: vcpu.h:61
l4_uint16_t state
Current vCPU state.
Definition: vcpu.h:54
An event (e.g. IRQ) is pending.
Definition: vcpu.h:87
l4_vcpu_regs_t r
Register state.
Definition: vcpu.h:51
Debug exception enabled.
Definition: vcpu.h:76
State flags of a vCPU.
Definition: vcpu.h:71
IRQs (events) enabled.
Definition: vcpu.h:73
l4_umword_t entry_ip
IP for entry.
Definition: vcpu.h:62
vCPU message registers.
Definition: __vcpu-arch.h:63
l4_uint16_t saved_state
Saved vCPU state.
Definition: vcpu.h:55
vCPU registers.
Definition: __vcpu-arch.h:39
l4_uint16_t sticky_flags
Pending flags.
Definition: vcpu.h:56
#define L4_NOTHROW
Mark a function declaration and definition as never throwing an exception.
Definition: compiler.h:185
l4_cap_idx_t user_task
User task to use.
Definition: vcpu.h:59