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