summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorThomas Bauereiss2018-05-04 17:46:10 +0100
committerThomas Bauereiss2018-05-09 14:19:57 +0100
commitc6710bb09c1d492b4434f0b3b375750275b4d4b5 (patch)
tree2a8ce2dde66ff04cea5c22414e2ab844cf998b85 /lib
parentc3f3642dfa5647685ae3dea86beeef8abc27f026 (diff)
Run ARM built-in tests for Lem backend (via OCaml)
Diffstat (limited to 'lib')
-rw-r--r--lib/vector_dec.sail2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 1307bb56..17603e03 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -68,11 +68,13 @@ val vector_update = {
val add_bits = {
ocaml: "add_vec",
+ lem: "add_vec",
c: "add_bits"
} : forall 'n. (bits('n), bits('n)) -> bits('n)
val add_bits_int = {
ocaml: "add_vec_int",
+ lem: "add_vec_int",
c: "add_bits_int"
} : forall 'n. (bits('n), int) -> bits('n)