1open arm_progLib; 2open arm_saved_specsTheory; 3 4val () = arm_progLib.loadSpecs arm_saved_specsTheory.saved_specs; 5 6use "arm_tests.sml"; 7 8val fails = ref ([]:string list); 9 10fun attempt hex = 11 arm_spec_hex hex 12 handle HOL_ERR _ => (fails := hex::(!fails); [TRUTH]); 13 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