diff options
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 3aef9d3b..648a61bd 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -180,6 +180,7 @@ let rec extern_mem_value mode v = match v with | Interp.V_vector fst inc bits -> (to_bytes (bitls_from_ibits bits), Nothing) | Interp.V_vector_sparse fst stop inc bits default -> extern_mem_value mode (Interp_lib.fill_in_sparse v) + | _ -> Assert_extra.failwith ("extern_mem_value received non-externable value " ^ (Interp.string_of_value v)) end let rec extern_ifield_value v = match v with |