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