diff options
| author | Christopher Pulte | 2017-03-24 11:50:02 +0000 |
|---|---|---|
| committer | Christopher Pulte | 2017-03-24 11:50:02 +0000 |
| commit | 4f31d4d7f0e1c5d77d65fee14f4fb8e149201e73 (patch) | |
| tree | 0d1c4224bee76a846410e5d1068d04894a9d709f /src/lem_interp | |
| parent | 68f22b52e40a8e6ea8b99d514faf3310547e63e6 (diff) | |
Print tracking information for V_track, hopefully fix extern_vector_value, fix sail_values bug.
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp.lem | 2 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 543b7639..24f624e3 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -153,7 +153,7 @@ let rec {ocaml} string_of_value v = match v with | V_unknown -> "Unknown" | V_register r -> string_of_reg_form r | V_register_alias _ _ -> "register_as_alias" - | V_track v rs -> (*"tainted by {" ^ (list_to_string string_of_reg_form "," []) ^ "} --" ^*) (string_of_value v) + | V_track v rs -> "tainted by {" ^ (list_to_string string_of_reg_form "," []) ^ "} --" ^ (string_of_value v) end let ~{ocaml} string_of_value _ = "" diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 03de0123..aad7418d 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -256,6 +256,7 @@ let rec extern_vector_value v = match v with | Interp.V_vector_sparse _fst _stop _inc _bits _default -> Interp_lib.fill_in_sparse v $> extern_vector_value + | Interp.V_track v _ -> extern_vector_value v | _ -> Assert_extra.failwith ("extern_vector_value received non-externable value " ^ (Interp.string_of_value v)) end |