1signature arm_stepLib = 2sig 3 val BIT_THMS_CONV: Conv.conv 4 val arm_eval: string -> bool list * Term.term -> Thm.thm 5 val arm_instruction: Term.term list -> string list 6 val arm_step: string -> string -> Thm.thm list 7 val arm_step_code: string -> string quotation -> Thm.thm list list 8 val arm_step_hex: string -> string -> Thm.thm list 9 val arm_decode: Term.term list -> bool list * Term.term -> Thm.thm list 10 val arm_decode_hex: string -> string -> Thm.thm list 11 val hex_to_bits_32: string -> Term.term list 12 val list_instructions: unit -> string list 13 val print_instructions: unit -> unit 14 15 (* 16 17 open arm_stepLib 18 val () = print_instructions () 19 val ev = arm_step "v7,vfp" 20 fun pev s = (print (s ^ "\n"); Count.apply ev s); 21 val _ = Count.apply (List.map ev) (list_instructions ()) 22 val _ = Count.apply (List.map (Lib.total pev)) (list_instructions ()) 23 ev "LDR (+reg,pre)" 24 25 *) 26end 27