1243750Srwatsonopen arm_progLib;
2243750Srwatsonopen arm_saved_specsTheory;
3243750Srwatson
4156283Srwatsonval () = arm_progLib.loadSpecs arm_saved_specsTheory.saved_specs;
5185573Srwatson
6185573Srwatsonuse "arm_tests.sml";
7185573Srwatson
8185573Srwatsonval fails = ref ([]:string list);
9185573Srwatson
10156283Srwatsonfun attempt hex =
11161630Srwatson   arm_spec_hex hex
12161630Srwatson   handle HOL_ERR _ => (fails := hex::(!fails); [TRUTH]);
13161630Srwatson
14val () = (List.map attempt arm_tests; print "Done.\n")
15
16val failed = !fails
17
18val dec = arm_stepLib.arm_decode_hex ""
19
20val l = List.map dec failed
21