summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp/interp.lem')
-rw-r--r--src/lem_interp/interp.lem14
1 files changed, 7 insertions, 7 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 1a97f5db..7cdc5149 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -168,13 +168,6 @@ let reg_size reg =
end
end
-let vector_length v = match v with
- | V_vector n inc vals -> List.length vals
- | V_vector_sparse n m inc vals def -> m
- | V_lit _ -> 1
- | _ -> 0
-end
-
(*Constant unit value, for use in interpreter *)
let unitv = V_lit (L_aux L_unit Unknown)
@@ -458,6 +451,13 @@ let rec binary_taint thunk vall valr =
| (vl,vr) -> thunk vl vr
end
+let vector_length v = match (detaint v) with
+ | V_vector n inc vals -> List.length vals
+ | V_vector_sparse n m inc vals def -> m
+ | V_lit _ -> 1
+ | _ -> 0
+end
+
val access_vector : value -> nat -> value
let access_vector v n =
retaint v (match (detaint v) with