summaryrefslogtreecommitdiff
path: root/src/value.ml
diff options
context:
space:
mode:
authorJon French2018-10-16 16:25:39 +0100
committerJon French2018-10-16 17:03:30 +0100
commit315fccb1b063f5ffa131b5a761fa1b2d33fa130f (patch)
treeeed4db4a25e3c1c44d7394f4749ef1612c7af105 /src/value.ml
parent45ce9105ce90efeccb9d0a183390027cdb1536af (diff)
parent58c1292f2f5a54f069e00e4065c00936963db8cd (diff)
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'src/value.ml')
-rw-r--r--src/value.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/value.ml b/src/value.ml
index 6c9990a1..157c16fc 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -219,6 +219,10 @@ let value_string_drop = function
| [v1; v2] -> V_string (Sail_lib.string_drop (coerce_string v1, coerce_int v2))
| _ -> failwith "value string_drop"
+let value_string_take = function
+ | [v1; v2] -> V_string (Sail_lib.string_take (coerce_string v1, coerce_int v2))
+ | _ -> failwith "value string_take"
+
let value_string_length = function
| [v] -> V_int (coerce_string v |> Sail_lib.string_length)
| _ -> failwith "value string_length"
@@ -549,6 +553,7 @@ let primops =
("eq_string", value_eq_string);
("string_startswith", value_string_startswith);
("string_drop", value_string_drop);
+ ("string_take", value_string_take);
("string_length", value_string_length);
("eq_bit", value_eq_bit);
("eq_anything", value_eq_anything);