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