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#include <autoconf.h> 14#include <sel4platsupport/gen_config.h> 15 16#ifdef CONFIG_LIB_SEL4_PLAT_SUPPORT_START 17 18.text 19 20/* 21 * Image Entry point. 22 */ 23.global _start 24_start: 25 /* Setup a stack for ourselves. */ 26 ldr x19, =_stack_top 27 mov sp, x19 28 29 /* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'. */ 30 bl seL4_InitBootInfo 31 32 /* Call constructors and other initialisation functions. */ 33 bl _init 34 35 /* Call main. */ 36 bl main 37 b exit 38 39/* Stack for the image. */ 40.bss 41.balign 8 42_stack_bottom: 43.space 16384 44_stack_top: 45 46#endif /* CONFIG_LIB_SEL4_PLAT_SUPPORT_START */ 47