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