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#pragma once 14 15#include <sel4/sel4.h> 16#include <stddef.h> 17#include <utils/util.h> 18 19static UNUSED const char *register_names[] = { 20 "eip", 21 "esp", 22 "eflags", 23 "eax", 24 "ebx", 25 "ecx", 26 "edx", 27 "esi", 28 "edi", 29 "ebp", 30 "fs_base", 31 "gs_base", 32}; 33compile_time_assert(register_names_correct_size, sizeof(register_names) == sizeof(seL4_UserContext)); 34 35/* assert that register_names correspond to seL4_UserContext */ 36compile_time_assert(eip_correct_position, offsetof(seL4_UserContext, eip) == 0); 37compile_time_assert(esp_correct_position, offsetof(seL4_UserContext, esp) == 1 * sizeof(seL4_Word)); 38compile_time_assert(eflags_correct_position, offsetof(seL4_UserContext, eflags) == 2 * sizeof(seL4_Word)); 39compile_time_assert(eax_correct_position, offsetof(seL4_UserContext, eax) == 3 * sizeof(seL4_Word)); 40compile_time_assert(ebx_correct_position, offsetof(seL4_UserContext, ebx) == 4 * sizeof(seL4_Word)); 41compile_time_assert(ecx_correct_position, offsetof(seL4_UserContext, ecx) == 5 * sizeof(seL4_Word)); 42compile_time_assert(edx_correct_position, offsetof(seL4_UserContext, edx) == 6 * sizeof(seL4_Word)); 43compile_time_assert(esi_correct_position, offsetof(seL4_UserContext, esi) == 7 * sizeof(seL4_Word)); 44compile_time_assert(edi_correct_position, offsetof(seL4_UserContext, edi) == 8 * sizeof(seL4_Word)); 45compile_time_assert(ebp_correct_position, offsetof(seL4_UserContext, ebp) == 9 * sizeof(seL4_Word)); 46compile_time_assert(fs_base_correct_position, offsetof(seL4_UserContext, fs_base) == 10 * sizeof(seL4_Word)); 47compile_time_assert(gs_base_correct_position, offsetof(seL4_UserContext, gs_base) == 11 * sizeof(seL4_Word)); 48 49