diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/mips_extras_ml.ml | 8 | ||||
| -rw-r--r-- | mips/run_embed.ml | 8 |
2 files changed, 13 insertions, 3 deletions
diff --git a/mips/mips_extras_ml.ml b/mips/mips_extras_ml.ml index 29f4a13d..2a624523 100644 --- a/mips/mips_extras_ml.ml +++ b/mips/mips_extras_ml.ml @@ -40,8 +40,12 @@ let _MEMr (addr, size) = begin let ret = ref (to_vec_dec_int (0, 0)) in for i = 0 to (s - 1) do let byte_addr = add_int_big_int i a in - let byte = Mem.find byte_addr !mips_mem in - let byte_vec = to_vec_dec_int (8, byte) in + let byte_vec = + try + let byte = Mem.find byte_addr !mips_mem in + to_vec_dec_int (8, byte) + with Not_found -> + to_vec_dec_undef_int 8 in ret := vector_concat byte_vec (!ret); (*printf "MEM [%s] -> %x %s %s\n" (big_int_to_hex byte_addr) byte (string_of_value byte_vec) (string_of_value !ret);*) done; diff --git a/mips/run_embed.ml b/mips/run_embed.ml index 42e36a6e..6a51063e 100644 --- a/mips/run_embed.ml +++ b/mips/run_embed.ml @@ -311,7 +311,13 @@ let time_it action arg = (finish_time -. start_time, ret) let rec debug_print_gprs start stop = - resultf "DEBUG MIPS REG %.2d 0x%s\n" start (big_int_to_hex64 (unsigned_big(vector_access Mips_model._GPR (big_int_of_int start)))); + let gpr_val = vector_access Mips_model._GPR (big_int_of_int start) in + let gpr_str = + if has_undef gpr_val then + "uuuuuuuuuuuuuuuu" + else + big_int_to_hex64 (unsigned_big(gpr_val)) in + resultf "DEBUG MIPS REG %.2d 0x%s\n" start gpr_str; if start < stop then debug_print_gprs (start + 1) stop else () |
