|
Last change
on this file since 491 was
437,
checked in by sacerdot, 10 years ago
|
- new function assembly_unlabelled_program
- the new function is now used in DoTest?.ma
|
|
File size:
773 bytes
|
| Line | |
|---|
| 1 | open BitVectors;; |
|---|
| 2 | open ASMInterpret;; |
|---|
| 3 | open Util;; |
|---|
| 4 | open MatitaPretty;; |
|---|
| 5 | |
|---|
| 6 | let hex = IntelHex.intel_hex_of_file Sys.argv.(1) in |
|---|
| 7 | let mem = IntelHex.process_intel_hex hex in |
|---|
| 8 | let status = ASMInterpret.load_mem mem ASMInterpret.initialize in |
|---|
| 9 | let mem_pretty_print status = |
|---|
| 10 | let rec aux status pc = |
|---|
| 11 | let instr, pc', cost = ASMInterpret.fetch status.ASMInterpret.code_memory pc in |
|---|
| 12 | print_string $ pp_matita_instruction instr; |
|---|
| 13 | if int_of_vect pc' <= 200 then (* DPM: hardcoded on a case-by-case basis *) |
|---|
| 14 | begin |
|---|
| 15 | print_string ";\n "; |
|---|
| 16 | aux status pc' |
|---|
| 17 | end |
|---|
| 18 | in |
|---|
| 19 | aux status status.ASMInterpret.pc |
|---|
| 20 | in |
|---|
| 21 | print_string "include \"ASM.ma\".\n\nndefinition test: List instruction ≝\n ["; |
|---|
| 22 | mem_pretty_print status; |
|---|
| 23 | print_endline "].\n @.\nnqed." |
|---|
| 24 | ;; |
|---|
Note: See
TracBrowser
for help on using the repository browser.
