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 <sel4test/test.h>
14#include "../test.h"
15#include "../helpers.h"
16
17#define MIN_EXPECTED_ALLOCATIONS 100
18
19int test_trivial(env_t env)
20{
21    test_geq(2, 1);
22    return sel4test_get_result();
23}
24DEFINE_TEST(TRIVIAL0000, "Ensure the test framework functions", test_trivial, true)
25
26int test_allocator(env_t env)
27{
28    /* Perform a bunch of allocations and frees */
29    vka_object_t endpoint;
30    int error;
31
32    for (int i = 0; i < MIN_EXPECTED_ALLOCATIONS; i++) {
33        error = vka_alloc_endpoint(&env->vka, &endpoint);
34        test_error_eq(error, 0);
35        test_assert(endpoint.cptr != 0);
36        vka_free_object(&env->vka, &endpoint);
37    }
38
39    return sel4test_get_result();
40}
41DEFINE_TEST(TRIVIAL0001, "Ensure the allocator works", test_allocator, true)
42DEFINE_TEST(TRIVIAL0002, "Ensure the allocator works more than once", test_allocator, true)
43