From d5df03ced568dade879f19331e4fa668aaee4bc3 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Fri, 7 Nov 2014 14:51:31 +0000
Subject: more num_to_bits

---
 src/lem_interp/interp_inter_imp.lem | 16 +---------------
 1 file changed, 1 insertion(+), 15 deletions(-)

(limited to 'src')

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 1227a4a8..768ef2de 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -30,7 +30,7 @@ end
 		   
 let intern_value v = match v with
   | Bitvector [true] _ _ -> Interp.V_lit (L_aux L_one Interp_ast.Unknown)
-  | Bitvector [false] _ _ -> Interp.V_lit (L_aux L_zero Interp_ast.Unknown)
+  | Bitvector [false] _ _ -> Interp.V_lit (L_aux L_(*TODO KG Needs to be an actualy error, as must mean that a variable is multiplied by a variable, somewhere *)zero Interp_ast.Unknown)
   | Bitvector bs inc fst   -> Interp.V_vector fst inc  (to_bits bs)
   | Bytevector bys -> Interp.V_vector 0 true 
     (List.concat (List.map (fun by -> 
@@ -44,20 +44,6 @@ let intern_value v = match v with
 end
 
 let num_to_bits size kind num =
-  match kind with
-    | Bitv -> Bitvector (match (Interp_lib.to_vec_inc 
-				  (Interp.V_tuple([Interp.V_lit(L_aux (L_num size) Interp_ast.Unknown);
-						   Interp.V_lit(L_aux (L_num (integerFromNat num)) Interp_ast.Unknown)]))) with
-	| Interp.V_vector _ _ bits -> from_bits bits end) true 0
-    | Bytev -> 
-      Bytevector (match (Interp_lib.to_vec_inc 
-			   (Interp.V_tuple([Interp.V_lit(L_aux (L_num size) Interp_ast.Unknown);
-					    Interp.V_lit(L_aux (L_num (integerFromNat num)) Interp_ast.Unknown)]))) with
-	| Interp.V_vector _ _ bits -> (to_bytes (from_bits bits)) end)
-end
-
-
-let num_to_bits_correct size kind num =
   match kind with
     | Bitv -> Bitvector (match (Interp_lib.to_vec_inc 
 				  (Interp.V_tuple([Interp.V_lit(L_aux (L_num (integerFromNat size)) Interp_ast.Unknown);
-- 
cgit v1.2.3