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