Add test for issue 286 (#539)

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

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/crates/flux-tests/tests/neg/surface/arr02.rs b/crates/flux-tests/tests/neg/surface/arr02.rs
@@ -14,3 +14,10 @@ fn test01() -> i32 {
     *arr[1] += 1;
     v1 //~ ERROR refinement type
 }
+
+#[flux::sig(fn() -> i32{v: v < 0})]
+fn test02() -> i32 {
+    let v = 42;
+    let arr = [&v, &v];
+    *arr[0] //~ ERROR refinement type
+}
diff --git a/crates/flux-tests/tests/pos/surface/arr02.rs b/crates/flux-tests/tests/pos/surface/arr02.rs
@@ -14,3 +14,10 @@ fn test01() -> i32 {
     *arr[1] += 1;
     v1
 }
+
+#[flux::sig(fn() -> i32{v: v >= 0})]
+fn test02() -> i32 {
+    let v = 42;
+    let arr = [&v, &v];
+    *arr[0]
+}