diff options
| author | Robert Norton | 2018-11-19 14:44:42 +0000 |
|---|---|---|
| committer | Robert Norton | 2018-11-19 15:01:01 +0000 |
| commit | 1bc81fa6dcafcfe24fce3685c2eb61f882e6b65c (patch) | |
| tree | 5cd34da665f25ae90dec49bb23ec82591163a4ff /lib | |
| parent | 6e4cd778ab07aff67497d320e2e345ecdbace217 (diff) | |
Add missing constraints on bitvector_access, with regression test.Fixes #24.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/vector_dec.sail | 2 | ||||
| -rw-r--r-- | lib/vector_inc.sail | 2 |
2 files changed, 2 insertions, 2 deletions
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", |