diff options
| author | Kathy Gray | 2014-11-07 14:51:31 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-11-07 14:51:31 +0000 |
| commit | d5df03ced568dade879f19331e4fa668aaee4bc3 (patch) | |
| tree | 6b611dff6a9c22f2866a209d2da09aaf4dc3cf53 /src/lem_interp/interp_inter_imp.lem | |
| parent | 32c017a6c326c4861ca6f548a9648cfb25af14e5 (diff) | |
more num_to_bits
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 16 |
1 files changed, 1 insertions, 15 deletions
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 -> @@ -46,20 +46,6 @@ 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); Interp.V_lit(L_aux (L_num num) Interp_ast.Unknown)]))) with | Interp.V_vector _ _ bits -> from_bits bits end) true 0 |