1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12#pragma once 13 14#include <sel4/sel4.h> 15 16static inline int seL4_ARCH_PageDirectory_Clean_Data(seL4_CPtr root, seL4_Word start, seL4_Word end) 17{ 18 return seL4_ARM_PageDirectory_Clean_Data(root, start, end); 19} 20 21static inline int seL4_ARCH_PageDirectory_Invalidate_Data(seL4_CPtr root, seL4_Word start, seL4_Word end) 22{ 23 return seL4_ARM_PageDirectory_Invalidate_Data(root, start, end); 24} 25 26static inline int seL4_ARCH_PageDirectory_CleanInvalidate_Data(seL4_CPtr root, seL4_Word start, seL4_Word end) 27{ 28 return seL4_ARM_PageDirectory_CleanInvalidate_Data(root, start, end); 29} 30 31static inline int seL4_ARCH_PageDirectory_Unify_Instruction(seL4_CPtr root, seL4_Word start, seL4_Word end) 32{ 33 return seL4_ARM_PageDirectory_Unify_Instruction(root, start, end); 34} 35 36