Add test for issue 158 (#540)

flux-rs · Oct 11, 2023 · 521260d · 521260d
1 parent 05a937e
commit 521260d
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 0 deletions.
diff --git a/crates/flux-tests/tests/neg/surface/issue-158.rs b/crates/flux-tests/tests/neg/surface/issue-158.rs
@@ -0,0 +1,15 @@
+#[path = "../../lib/rvec.rs"]
+mod rvec;
+
+use rvec::RVec;
+
+#[flux::refined_by(size:int)]
+pub struct Bob {
+    #[flux::field(RVec<i32{v: v > 0}>[@size])]
+    elems: RVec<i32>,
+}
+
+#[flux::sig(fn(&mut Bob{v: v.size > 0}) -> ())]
+pub fn test(bob: &mut Bob) {
+    bob.elems[0] = 0; //~ ERROR refinement type
+}
diff --git a/crates/flux-tests/tests/pos/structs/issue-158.rs b/crates/flux-tests/tests/pos/structs/issue-158.rs
@@ -0,0 +1,15 @@
+#[path = "../../lib/rvec.rs"]
+mod rvec;
+
+use rvec::RVec;
+
+#[flux::refined_by(size:int)]
+pub struct Bob {
+    #[flux::field(RVec<i32{v: v >= 0}>[@size])]
+    elems: RVec<i32>,
+}
+
+#[flux::sig(fn(&mut Bob{v: v.size > 0}) -> ())]
+pub fn test(bob: &mut Bob) {
+    bob.elems[0] = 0;
+}