1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory global_asm_stmt 8imports "CParser.CTranslation" "AsmRefine.GlobalsSwap" 9begin 10 11declare [[populate_globals=true]] 12 13typedecl machine_state 14typedecl cghost_state 15 16external_file "global_asm_stmt.c" 17install_C_file "global_asm_stmt.c" 18 [machinety=machine_state, ghostty=cghost_state] 19 20setup \<open>DefineGlobalsList.define_globals_list_i 21 "global_asm_stmt.c" @{typ globals}\<close> 22 23locale g_asm_target 24 = global_asm_stmt_global_addresses 25begin 26 27abbreviation 28 "globals_list \<equiv> global_asm_stmt_global_addresses.global_data_list" 29lemmas global_data_defs = global_asm_stmt_global_addresses.global_data_defs 30 31end 32 33end 34