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