1signature m0_stepLib = 2sig 3 val thumb_instruction: Term.term -> string 4 val thumb_step: bool * bool -> string -> Thm.thm list 5 val thumb_step_code: bool * bool -> string quotation -> Thm.thm list list 6 val thumb_step_hex: bool * bool -> string -> Thm.thm list 7 val thumb_decode: bool -> Term.term -> Thm.thm list 8 val thumb_decode_hex: bool -> string -> Thm.thm list 9 val hex_to_bits: string -> Term.term 10 val list_instructions: unit -> (string * Term.term) list 11 val print_instructions: unit -> unit 12 13 (* 14 15 open m0_stepLib 16 val () = print_instructions () 17 val ev = thumb_step (true, true) 18 fun pev s = (print (s ^ "\n"); Count.apply ev s); 19 val _ = Count.apply (List.map ev) (list_instructions ()) 20 val _ = Count.apply (List.map (Lib.total pev)) (list_instructions ()) 21 ev "POP; 2" 22 ev "ADD (pc)" 23 24 *) 25end 26