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#pragma once 14 15#include <autoconf.h> 16 17#include <sel4/sel4.h> 18#include <sel4/types.h> 19 20/* An implementation of printf that you can safely call from within syscall 21 * stubs. 22 */ 23int 24debug_safe_printf(const char *format, ...) 25__attribute__((format(printf, 1, 2))) 26__attribute__((no_instrument_function)); 27 28void debug_cap_identify(seL4_CPtr cap); 29 30static inline int debug_cap_is_valid(seL4_CPtr cap) 31{ 32 return (0 != seL4_DebugCapIdentify(cap)); 33} 34 35static inline int debug_cap_is_endpoint(seL4_CPtr cap) 36{ 37 // there is kernel/generated/arch/object/structures_gen.h that defines 38 // cap_endpoint_cap = 4, but we can't include it here 39 return (4 == seL4_DebugCapIdentify(cap)); 40} 41 42static inline int debug_cap_is_notification(seL4_CPtr cap) 43{ 44 // there is kernel/generated/arch/object/structures_gen.h that defines 45 // cap_notification_cap = 6, but we can't include it here 46 return (6 == seL4_DebugCapIdentify(cap)); 47} 48 49 50void debug_print_bootinfo(seL4_BootInfo *info); 51 52