1open HolKernel Parse boolLib bossLib;
2open decompileLib backgroundLib;
3
4val _ = new_theory "decompile_test";
5
6(*
7
8(* RISC-V kernel *)
9
10val base_name = "seL4-kernel/riscv/kernel-riscv"
11val fast = false;
12val res = decomp base_name fast "trap_entry";
13
14val _ = not (!has_failures) orelse failwith "There were failures.";
15
16(* ARM kernel *)
17
18val base_name = "seL4-kernel/arm/kernel"
19val fast = false;
20val ignore_names = "fastpath_restore,restore_user_context,_start,arm_prefetch_abort_exception,arm_data_abort_exception";
21val res = decomp base_name fast ignore_names;
22
23val _ = not (!has_failures) orelse failwith "There were failures.";
24
25*)
26
27(* RISC-V example *)
28
29val base_name = "seL4-kernel/riscv/kernel-riscv"
30val fast = false;
31val res = decomp_only base_name fast
32  ["memzero", "memcpy", "write_slot", "emptySlot", "lookupSlot",
33   "resolveAddressBits"];
34
35val _ = not (!has_failures) orelse failwith "There were failures.";
36
37(* ARMv7 example *)
38
39val base_name = "loop/example";
40val fast = false;
41val ignore_names = "";
42val res = decomp base_name fast ignore_names;
43
44val _ = not (!has_failures) orelse failwith "There were failures.";
45
46(* ARM-M0 *)
47
48val base_name = "loop-m0/example";
49val fast = false;
50val ignore_names = "";
51val res = decomp base_name fast ignore_names;
52
53val _ = export_theory();
54