diff options
| author | Kathy Gray | 2014-11-07 17:06:55 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-11-07 17:06:55 +0000 |
| commit | 4cb1d7ef1fbe429c6b04ea685e9c19b09a774263 (patch) | |
| tree | 1470e7e77993c2362de740eba4df130d99ef3cd1 /src/lem_interp/interp_inter_imp.lem | |
| parent | 08a7d0de5e844ae8ad2d7027a4da87df054b2a28 (diff) | |
Add integer_of_byte_list : list word8 -> integer
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 3c076eae..cacbda62 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -54,7 +54,13 @@ let num_to_bits size kind num = (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 -> (to_bytes (from_bits bits)) end) -end +end + +let integer_of_byte_list bytes = + let intv = intern_value (Bytevector bytes) in + match Interp_lib.to_num false intv with + | Interp.V_lit (L_aux (L_num n) _) -> n + end let extern_reg r slice = match (r,slice) with | (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x |
