1// SPDX-License-Identifier: GPL-2.0
2#define BUILD_VDSO32
3
4#ifndef CONFIG_CC_OPTIMIZE_FOR_SIZE
5#undef CONFIG_OPTIMIZE_INLINING
6#endif
7
8#ifdef CONFIG_X86_64
9
10/*
11 * in case of a 32 bit VDSO for a 64 bit kernel fake a 32 bit kernel
12 * configuration
13 */
14#undef CONFIG_64BIT
15#undef CONFIG_X86_64
16#undef CONFIG_PGTABLE_LEVELS
17#undef CONFIG_ILLEGAL_POINTER_VALUE
18#undef CONFIG_SPARSEMEM_VMEMMAP
19#undef CONFIG_NR_CPUS
20
21#define CONFIG_X86_32 1
22#define CONFIG_PGTABLE_LEVELS 2
23#define CONFIG_PAGE_OFFSET 0
24#define CONFIG_ILLEGAL_POINTER_VALUE 0
25#define CONFIG_NR_CPUS 1
26
27#define BUILD_VDSO32_64
28
29#endif
30
31#include "../vclock_gettime.c"
32