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 <allocman/cspace/simple1level.h>
14#include <allocman/util.h>
15#include <allocman/allocman.h>
16#include <sel4/sel4.h>
17
18void cspace_simple1level_create(cspace_simple1level_t *cspace, struct cspace_simple1level_config config)
19{
20    *cspace = (cspace_simple1level_t) {
21        .config = config, .current_slot = config.first_slot
22    };
23}
24
25int _cspace_simple1level_alloc(allocman_t *alloc, void *_cspace, cspacepath_t *slot)
26{
27    cspace_simple1level_t *cspace = (cspace_simple1level_t*)_cspace;
28
29    if (cspace->current_slot == cspace->config.end_slot) {
30        return 1;
31    }
32
33    *slot = _cspace_simple1level_make_path(cspace, cspace->current_slot++);
34    return 0;
35}
36
37void _cspace_simple1level_free(allocman_t *alloc, void *_cspace, const cspacepath_t *slot)
38{
39    /* We happily ignore this */
40}
41