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
12 exception_t benchmark_arch_map_logBuffer(word_t frame_cptr);
13 #endif /* CONFIG_KERNEL_LOG_BUFFER */
14 
15