# CONFIG_VDSO is not set