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