#include <linux/init.h>
#include <linux/smp.h>
#include <linux/kernel.h>
#include <linux/mm_types.h>
#include <linux/elf.h>
#include <asm/processor.h>
#include <asm/vdso.h>
#ifdef CONFIG_COMPAT_VDSO
#define VDSO_DEFAULT …
#else
#define VDSO_DEFAULT …
#endif
unsigned int __read_mostly vdso32_enabled = …;
static int __init vdso32_setup(char *s)
{ … }
__setup(…);
#ifdef CONFIG_X86_32
__setup_param("vdso=", vdso_setup, vdso32_setup, 0);
#endif
#ifdef CONFIG_X86_64
#ifdef CONFIG_SYSCTL
#include <linux/sysctl.h>
static struct ctl_table abi_table2[] = …;
static __init int ia32_binfmt_init(void)
{ … }
__initcall(ia32_binfmt_init);
#endif
#endif