1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12/* 13 * A default crt0 for ia32. It does the bare minimum required to get into 14 * main() with a sensible C environment. 15 * 16 * This file will only be linked in if: 17 * - no other file already provides a _start symbol, and 18 * - _start is an undefined external symbol (force this by passing 19 * "-u _start" to ld). 20 */ 21 22#define __ASM__ 23#include <autoconf.h> 24#include <sel4platsupport/gen_config.h> 25 26#ifdef CONFIG_LIB_SEL4_PLAT_SUPPORT_START 27 28#include <sel4/arch/constants.h> 29 30 .global _start 31 32 .text 33 34.align 0x1000 35_start: 36 leaq _stack_top, %rsp 37 38# setup the bootinfo 39 movq %rbx, %rdi 40 call seL4_InitBootInfo 41 42 /* Call constructors and other initialisation functions. */ 43 call _init 44 45 call main 46# the return value is in rax 47 movq %rax, %rdi 48 call exit 49 501: jmp 1b 51 52 .bss 53 .balign 8 54 55_stack_bottom: 56 .space 16384 57_stack_top: 58 59#endif /* CONFIG_LIB_SEL4_PLAT_SUPPORT_START */ 60