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