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/* This file contains tests related to TCB syscalls. */
14
15#include <stdio.h>
16#include <sel4/sel4.h>
17#include <sel4test/testutil.h>
18#include <sel4test/macros.h>
19
20#include "../helpers.h"
21
22int test_tcb_null_cspace_configure(env_t env)
23{
24    helper_thread_t thread;
25    int error;
26
27    create_helper_thread(env, &thread);
28
29    /* This should fail because we're passing an invalid CSpace cap. */
30    error = api_tcb_configure(get_helper_tcb(&thread), 0, seL4_CapNull,
31                              seL4_CapNull, seL4_CapNull,
32                              0, env->page_directory,
33                              0, 0, 0);
34
35    cleanup_helper(env, &thread);
36
37    return error ? sel4test_get_result() : FAILURE;
38}
39DEFINE_TEST(THREADS0004, "seL4_TCB_Configure with a NULL CSpace should fail", test_tcb_null_cspace_configure, true)
40
41int test_tcb_null_cspace_setspace(env_t env)
42{
43    helper_thread_t thread;
44    int error;
45
46    create_helper_thread(env, &thread);
47
48    /* This should fail because we're passing an invalid CSpace cap. */
49    error = api_tcb_set_space(get_helper_tcb(&thread), 0, seL4_CapNull,
50                              0, env->page_directory,
51                              0);
52
53    cleanup_helper(env, &thread);
54
55    return error ? sel4test_get_result() : FAILURE;
56}
57DEFINE_TEST(THREADS0005, "seL4_TCB_SetSpace with a NULL CSpace should fail", test_tcb_null_cspace_setspace, true)
58
59