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 13#include <assert.h> 14#include <sel4/sel4.h> 15#include <stdint.h> 16#include <stdlib.h> 17#include <vka/cspacepath_t.h> 18#include <vka/null-vka.h> 19#include <vka/vka.h> 20 21static int cspace_alloc(void *data, seL4_CPtr *res) 22{ 23 return -1; 24} 25 26static void cspace_make_path(void *data, seL4_CPtr slot, cspacepath_t *res) 27{ 28} 29 30static void cspace_free(void *data, seL4_CPtr slot) 31{ 32} 33 34static int utspace_alloc(void *data, const cspacepath_t *dest, seL4_Word type, 35 seL4_Word size_bits, seL4_Word *res) 36{ 37 return -1; 38} 39 40static int utspace_alloc_maybe_device(void *data, const cspacepath_t *dest, seL4_Word type, 41 seL4_Word size_bits, bool can_use_dev, seL4_Word *res) 42{ 43 return -1; 44} 45 46static int utspace_alloc_at(void *data, const cspacepath_t *dest, seL4_Word type, 47 seL4_Word size_bits, uintptr_t paddr, seL4_Word *res) 48{ 49 return -1; 50} 51 52static void utspace_free(void *data, seL4_Word type, seL4_Word size_bits, 53 seL4_Word target) 54{ 55} 56 57static uintptr_t utspace_paddr(void *data, seL4_Word target, seL4_Word type, seL4_Word size_bits) 58{ 59 return VKA_NO_PADDR; 60} 61 62void vka_init_nullvka(vka_t *vka) 63{ 64 assert(vka != NULL); 65 *vka = (vka_t) { 66 .data = NULL, /* not required */ 67 .cspace_alloc = cspace_alloc, 68 .cspace_make_path = cspace_make_path, 69 .utspace_alloc = utspace_alloc, 70 .utspace_alloc_maybe_device = utspace_alloc_maybe_device, 71 .utspace_alloc_at = utspace_alloc_at, 72 .cspace_free = cspace_free, 73 .utspace_free = utspace_free, 74 .utspace_paddr = utspace_paddr 75 }; 76} 77