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 #undef CONFIG_X86_PPRO_FENCE
9 
10 #ifdef CONFIG_X86_64
11 
12 /*
13  * in case of a 32 bit VDSO for a 64 bit kernel fake a 32 bit kernel
14  * configuration
15  */
16 #undef CONFIG_64BIT
17 #undef CONFIG_X86_64
18 #undef CONFIG_PGTABLE_LEVELS
19 #undef CONFIG_ILLEGAL_POINTER_VALUE
20 #undef CONFIG_SPARSEMEM_VMEMMAP
21 #undef CONFIG_NR_CPUS
22 
23 #define CONFIG_X86_32 1
24 #define CONFIG_PGTABLE_LEVELS 2
25 #define CONFIG_PAGE_OFFSET 0
26 #define CONFIG_ILLEGAL_POINTER_VALUE 0
27 #define CONFIG_NR_CPUS 1
28 
29 #define BUILD_VDSO32_64
30 
31 #endif
32 
33 #include "../vclock_gettime.c"
34