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.

---
 lib/vector_dec.sail | 2 +-
 lib/vector_inc.sail | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 8abcd218..7011a55c 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -63,7 +63,7 @@ val bitvector_access = {
   lem: "access_vec_dec",
   coq: "access_vec_dec",
   c: "vector_access"
-} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit
+} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit
 
 val plain_vector_access = {
   ocaml: "access",
diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail
index b295c92c..042a6324 100644
--- a/lib/vector_inc.sail
+++ b/lib/vector_inc.sail
@@ -61,7 +61,7 @@ val bitvector_access = {
   lem: "access_vec_inc",
   coq: "access_vec_inc",
   c: "vector_access"
-} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit
+} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit
 
 val plain_vector_access = {
   ocaml: "access",
-- 
cgit v1.2.3