add verify_partial regression tests for viperproject#729 and viperp…

…roject#738

prusti-tests/tests/verify_partial/fail/issues/issue-729-1.rs

@@ -0,0 +1,33 @@
+// error-pattern: Precondition of function snap$__$TY$__struct$m_A$Snap$struct$m_A might not hold
+// ^^^^^^^^^^^^^^ this is an actual assertion, see:
+// <https://rustc-dev-guide.rust-lang.org/tests/adding.html#when-error-line-cannot-be-specified>
+// FIXME: https://github.com/viperproject/prusti-dev/issues/729
+#![allow(unused_comparisons)]
+extern crate prusti_contracts;
+use prusti_contracts::*;
+
+pub struct A {
+    inner: [usize; 4],
+}
+
+impl A {
+    #[pure]
+    #[requires(index < self.inner.len())]
+    pub fn is_valid(&self, index: usize) -> bool {
+        self.inner[index] <= isize::MAX as usize
+    }
+
+    #[pure]
+    #[ensures(forall(|i: usize| (result && index < self.inner.len() && 0 <= i && i <= index) ==> (self.is_valid(i))) )]
+    pub fn test(&self, index: usize) -> bool {
+        match index {
+            index if 0 < index && index < self.inner.len() => {
+                self.is_valid(index) && self.test(index - 1)
+            }
+            index if index == 0 => self.is_valid(index),
+            _ => false,
+        }
+    }
+}
+
+fn main() {}

prusti-tests/tests/verify_partial/fail/issues/issue-738-1.rs

@@ -0,0 +1,29 @@
+use prusti_contracts::*;
+
+#[derive(Clone, Copy)]
+pub struct A {
+    count: isize,
+}
+
+impl A {
+    #[pure]
+    #[ensures(result <= isize::MAX as usize)]
+    pub const fn len(&self) -> usize {
+        if self.count < 0 {
+            ((1_isize + self.count) + isize::MAX) as usize
+        } else {
+            self.count as usize
+            //~^ ERROR value might not fit into the target type.
+            // FIXME: https://github.com/viperproject/prusti-dev/issues/738
+        }
+    }
+}
+
+#[pure]
+#[requires(slice.len() > 0)]
+#[requires(slice[0].len() == 0)]
+pub fn test(slice: &[A]) -> bool {
+    true
+}
+
+fn main() {}