1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6#pragma once 7 8#include <config.h> 9#include <arch/kernel/vspace.h> 10 11#ifdef CONFIG_KERNEL_LOG_BUFFER 12exception_t benchmark_arch_map_logBuffer(word_t frame_cptr); 13#endif /* CONFIG_KERNEL_LOG_BUFFER */ 14 15