1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#pragma once 8 9#include <config.h> 10#include <util.h> 11#include <arch/types.h> 12 13#define FORMAT(archetype, string_index, first_to_check) \ 14 __attribute__((format(archetype, string_index, first_to_check))) 15 16#if (defined CONFIG_DEBUG_BUILD) || (defined CONFIG_PRINTING) 17void putDebugChar(unsigned char c); 18#endif 19 20#ifdef CONFIG_DEBUG_BUILD 21/* io for dumping capdl */ 22unsigned char getDebugChar(void); 23#endif 24 25#ifdef CONFIG_PRINTING 26/* printf will result in output */ 27void putchar(char c); 28#define kernel_putchar(c) putchar(c) 29word_t kprintf(const char *format, ...) VISIBLE FORMAT(printf, 1, 2); 30word_t ksnprintf(char *str, word_t size, const char *format, ...); 31word_t puts(const char *s) VISIBLE; 32#define printf(args...) kprintf(args) 33#define snprintf(args...) ksnprintf(args) 34#else /* CONFIG_PRINTING */ 35/* printf will NOT result in output */ 36#define kernel_putchar(c) ((void)(0)) 37#define printf(args...) ((void)(0)) 38#define puts(s) ((void)(0)) 39#endif /* CONFIG_PRINTING */ 40