diff options
| author | Brian Campbell | 2018-04-09 15:24:32 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-04-09 16:05:59 +0100 |
| commit | 86402c298c24e47ae49de7fb9748f0a67aaa98d2 (patch) | |
| tree | 494942a66510f6cfbfec18443c7f5dc1ca3dbcee /src/state.ml | |
| parent | 0d77821e3617c6d7591ba1d68ab0fe90f8cb3c9c (diff) | |
Stop vector_typ_args_of from failing when order is a variable
Now it just returns the actual arguments and a separate function
calculates the start index when required.
Diffstat (limited to 'src/state.ml')
| -rw-r--r-- | src/state.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/state.ml b/src/state.ml index 8e024179..40ec80ad 100644 --- a/src/state.ml +++ b/src/state.ml @@ -157,7 +157,7 @@ let add_regval_conv id typ defs = let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with | Typ_app _ when is_vector_typ typ && not (mwords && is_bitvector_typ typ) -> - let _, size, ord, etyp = vector_typ_args_of typ in + let size, ord, etyp = vector_typ_args_of typ in let size = string_of_nexp (nexp_simp size) in let is_inc = if is_order_inc ord then "true" else "false" in let etyp_of, of_etyp = regval_convs_lem mwords etyp in |