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