diff options
| author | Kathy Gray | 2016-06-03 15:59:57 +0100 |
|---|---|---|
| committer | Kathy Gray | 2016-06-03 16:00:11 +0100 |
| commit | 33ce6cafbd7254b52fe5c6a2244f57bb6d4e7f42 (patch) | |
| tree | c844cef4866a3763430cd68f403dfe026e10277b /src | |
| parent | a77f59965a265cfe056c4048f6d63e1fbbc54950 (diff) | |
Mips file: removed some unnecessary parenthesis
Interp: trying to add some debugging to isolate bug
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp.lem | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index dccbe090..f3938453 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -13,6 +13,9 @@ open import Instruction_extractor type tannot = Interp_utilities.tannot +val debug_print : string -> unit +declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s + val intern_annot : tannot -> tannot let intern_annot annot = match annot with @@ -574,6 +577,7 @@ end val access_vector : value -> nat -> value let access_vector v n = + let _ = debug_print ("access_vector given " ^ string_of_value v ^ " and " ^ show n) in retaint v (match (detaint v) with | V_unknown -> V_unknown | V_lit (L_aux L_undef _) -> v @@ -1054,9 +1058,6 @@ let fix_up_nondet typ branches annot = (fun e -> E_aux (E_assign (LEXP_aux (LEXP_id redex_id) annot) e) annot) branches), Just "0") end -val debug_print : string -> unit -declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s - (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *) val match_pattern : top_level -> pat tannot -> value -> bool * bool * lenv let rec match_pattern t_level (P_aux p (_, annot)) value_whole = |