diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 12 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 45f91601..3c076eae 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -45,14 +45,14 @@ 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 + | 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 | 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 + Bytevector (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 -> (to_bytes (from_bits bits)) end) end diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 93194fe2..2422ccc5 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -230,7 +230,7 @@ type i_state_or_error = | Instr of instruction * instruction_state | Decode_error of decode_error -val num_to_bits : nat -> v_kind -> integer +val num_to_bits : nat -> v_kind -> integer -> value (** proposed: *) val nat_to_bytevector : nat -> list word8 |