541289a326
Originally building the kernel was largely considered to be done in one of two ways 1. Release build with no assertions, no debug symbols and no printing. This was generally considered to be a 'verified' build 2. Debug build with assertions, debug symbols and printing Since then various options were added, such as the 'code injection' option, which we wanted on builds that did not have assertions or other options that affected performance. As such it did not depend upon a debug build and had large warning signs saying that enabling this in a release build would not give you a verified or trusted kernel. Most recently the ability to print from the kernel in release mode was added. For the same reason that tying the ability to print with the performance reduction of various debugging was not always desireable. This change attempts to unify the current state and have a single top level option to enable a 'verification friendly' build. All other options (assertions, printing, code injection) then depend upon this configuration not being set.
35 lines
1,010 B
C
35 lines
1,010 B
C
/*
|
|
* Copyright 2014, General Dynamics C4 Systems
|
|
*
|
|
* This software may be distributed and modified according to the terms of
|
|
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
|
* See "LICENSE_GPLv2.txt" for details.
|
|
*
|
|
* @TAG(GD_GPL)
|
|
*/
|
|
|
|
#ifndef __MACHINE_IO_H
|
|
#define __MACHINE_IO_H
|
|
|
|
#include <config.h>
|
|
#include <util.h>
|
|
#include <arch/types.h>
|
|
#include <plat/machine/io.h>
|
|
|
|
#define FORMAT(archetype, string_index, first_to_check) \
|
|
__attribute__((format(archetype, string_index, first_to_check)))
|
|
|
|
#ifdef CONFIG_PRINTING
|
|
/* printf will result in output */
|
|
word_t kprintf(const char *format, ...) VISIBLE FORMAT(printf, 1, 2);
|
|
word_t puts(const char *s) VISIBLE;
|
|
word_t print_unsigned_long(unsigned long x, word_t ui_base) VISIBLE;
|
|
#define printf(args...) kprintf(args)
|
|
#else /* CONFIG_PRINTING */
|
|
/* printf will NOT result in output */
|
|
#define printf(args...) ((void)(0))
|
|
/* and neither will puts */
|
|
#define puts(s) ((void)(0))
|
|
#endif /* CONFIG_PRINTING */
|
|
|
|
#endif
|