diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 3c076eae..1227a4a8 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -46,6 +46,20 @@ 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 |