Add missing constraints on bitvector_access, with regression test.Fixes #24.

3 files changed, 29 insertions, 0 deletions

diff --git a/test/typecheck/pass/vec_length.sail b/test/typecheck/pass/vec_length.sail
new file mode 100644
index 00000000..078e266b
--- /dev/null
+++ b/test/typecheck/pass/vec_length.sail
@@ -0,0 +1,8 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  ()
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect
new file mode 100644
index 00000000..68a4ca70
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v1.sail", line 6, character 11 to line 6, character 15
+
+  let y = x[10];
+
+No overloadings for vector_access, tried:
+  bitvector_access:
+    Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_access:
+    Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v1.sail b/test/typecheck/pass/vec_length/v1.sail
new file mode 100644
index 00000000..735da89c
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1.sail
@@ -0,0 +1,8 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[10];
+  ()
+}
\ No newline at end of file