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