1/* 2 * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7#pragma once 8 9#include <sel4utils/vspace.h> 10#include <sel4utils/vspace_internal.h> 11 12static inline int guest_vspace_map_page_arch(vspace_t *vspace, seL4_CPtr cap, void *vaddr, seL4_CapRights_t rights, 13 int cacheable, size_t size_bits) 14{ 15 return sel4utils_map_page_ept(vspace, cap, vaddr, rights, cacheable, size_bits); 16} 17