1open HolKernel Parse boolLib bossLib; 2open arm8_decompLib 3 4val () = new_theory "arm8_decomp_demo"; 5 6val (test1_cert, test1_def) = arm8_decompile_no_status "test1" 7 `54000048 8 1b000001 9 ` 10 11val (test2_cert, test2_def) = arm8_decompile_code_no_status "test2" 12 `mov x1, #4 13 add x2, x3, x4 14 str x2, [x1, #8]! 15 ` 16 17val (test3_cert, test3_def) = arm8_decompLib.arm8_decompile_code "test3" 18 `loop: mul x1, x1, x2 19 subs x0, x0, #1 20 b.ne loop` 21 22val () = export_theory() 23