From 4f31d4d7f0e1c5d77d65fee14f4fb8e149201e73 Mon Sep 17 00:00:00 2001
From: Christopher Pulte
Date: Fri, 24 Mar 2017 11:50:02 +0000
Subject: Print tracking information for V_track, hopefully fix
 extern_vector_value, fix sail_values bug.

---
 src/lem_interp/interp.lem           | 2 +-
 src/lem_interp/interp_inter_imp.lem | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/lem_interp')

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
 
-- 
cgit v1.2.3