From 1bc81fa6dcafcfe24fce3685c2eb61f882e6b65c Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 19 Nov 2018 14:44:42 +0000
Subject: Add missing constraints on bitvector_access, with regression
 test.Fixes #24.

---
 test/typecheck/pass/vec_length.sail      |  8 ++++++++
 test/typecheck/pass/vec_length/v1.expect | 13 +++++++++++++
 test/typecheck/pass/vec_length/v1.sail   |  8 ++++++++
 3 files changed, 29 insertions(+)
 create mode 100644 test/typecheck/pass/vec_length.sail
 create mode 100644 test/typecheck/pass/vec_length/v1.expect
 create mode 100644 test/typecheck/pass/vec_length/v1.sail

(limited to 'test/typecheck')

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
-- 
cgit v1.2.3