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