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