RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

libsel4: Remove unused argument in seL4_VMEnter syscall

Browse Source 
This VCPU argument does not make sense given semantics of the VMEnter syscall,
and as a result the argument is ignored by the kernel.
This commit is contained in:
Adrian Danis
2017-09-06 15:48:35 +10:00
parent ad03c3348c
commit cfb30f34b9
2 changed files with 4 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
View File

@@ -505,14 +505,14 @@ seL4_Yield(void)
#ifdef CONFIG_VTX
LIBSEL4_INLINE_FUNC seL4_Word
seL4_VMEnter(seL4_CPtr vcpu, seL4_Word *sender)
seL4_VMEnter(seL4_Word *sender)
{
seL4_Word fault;
seL4_Word badge;
seL4_Word mr0 = seL4_GetMR(0);
seL4_Word mr1 = seL4_GetMR(1);
x86_sys_send_recv(seL4_SysVMEnter, vcpu, &badge, 0, &fault, &mr0, &mr1);
x86_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, &mr1);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);

4
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
View File

@@ -304,7 +304,7 @@ seL4_Yield(void)
#ifdef CONFIG_VTX
static inline seL4_Word
seL4_VMEnter(seL4_CPtr vcpu, seL4_Word *sender)
seL4_VMEnter(seL4_Word *sender)
{
seL4_Word fault;
seL4_Word badge;
@@ -313,7 +313,7 @@ seL4_VMEnter(seL4_CPtr vcpu, seL4_Word *sender)
seL4_Word mr2 = seL4_GetMR(2);
seL4_Word mr3 = seL4_GetMR(3);
x64_sys_send_recv(seL4_SysVMEnter, vcpu, &badge, 0, &fault, &mr0, &mr1, &mr2, &mr3);
x64_sys_send_recv(seL4_SysVMEnter, 0, &badge, 0, &fault, &mr0, &mr1, &mr2, &mr3);
seL4_SetMR(0, mr0);
seL4_SetMR(1, mr1);