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>
34 typedef struct l4_vcpu_state_t
35 {
36  l4_umword_t version;
37  l4_umword_t user_data[7];
44  l4_uint16_t _reserved;
50  l4_umword_t reserved_sp;
51  l4_vcpu_arch_state_t arch_state;
59 {
60  L4_VCPU_F_IRQ = 0x01,
66 };
73 {
75 };
82 {
85 };
98 L4_INLINE int
99 l4_vcpu_check_version(l4_vcpu_state_t const *vcpu) L4_NOTHROW;
101 /* IMPLEMENTATION: ------------------------------------------------*/
103 L4_INLINE int
104 l4_vcpu_check_version(l4_vcpu_state_t const *vcpu) L4_NOTHROW
105 {
106  return vcpu->version == L4_VCPU_STATE_VERSION;
107 }
State of a vCPU.
Definition: vcpu.h:34
Offset where extended state begins.
Definition: vcpu.h:83
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:39
struct l4_vcpu_state_t l4_vcpu_state_t
State of a vCPU.
Sticky flags of a vCPU.
Definition: vcpu.h:72
unsigned long l4_cap_idx_t
L4 Capability selector Type.
Definition: types.h:341
Offset where extended infos begin.
Definition: vcpu.h:84
User task will be used.
Definition: vcpu.h:64
FPU enabled.
Definition: vcpu.h:65
Page faults enabled.
Definition: vcpu.h:61
Offsets for vCPU state layouts.
Definition: vcpu.h:81
Exception enabled.
Definition: vcpu.h:62
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:48
l4_uint16_t state
Current vCPU state.
Definition: vcpu.h:41
An event (e.g. IRQ) is pending.
Definition: vcpu.h:74
l4_vcpu_regs_t r
Register state.
Definition: vcpu.h:38
Debug exception enabled.
Definition: vcpu.h:63
State flags of a vCPU.
Definition: vcpu.h:58
IRQs (events) enabled.
Definition: vcpu.h:60
l4_umword_t entry_ip
IP for entry.
Definition: vcpu.h:49
vCPU message registers.
Definition: __vcpu-arch.h:62
l4_uint16_t saved_state
Saved vCPU state.
Definition: vcpu.h:42
vCPU registers.
Definition: __vcpu-arch.h:38
l4_uint16_t sticky_flags
Pending flags.
Definition: vcpu.h:43
#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:46