From 1d6b1aa716d18dc37cd7eb2b3e2a948b1456b3d1 Mon Sep 17 00:00:00 2001
From: Zack Grannan <zgrannan@protonmail.com>
Date: Tue, 28 Nov 2023 09:03:36 -0800
Subject: [PATCH] More tests

---
 .../incorrect/old_in_pure_postcondition.rs    | 20 +++++++----------
 .../old_in_pure_postcondition_extern.rs       | 22 +++++++++++++++++++
 2 files changed, 30 insertions(+), 12 deletions(-)
 create mode 100644 prusti-tests/tests/verify/fail/incorrect/old_in_pure_postcondition_extern.rs

diff --git a/prusti-tests/tests/verify/fail/incorrect/old_in_pure_postcondition.rs b/prusti-tests/tests/verify/fail/incorrect/old_in_pure_postcondition.rs
index 01faa27f922..a1790f8eb60 100644
--- a/prusti-tests/tests/verify/fail/incorrect/old_in_pure_postcondition.rs
+++ b/prusti-tests/tests/verify/fail/incorrect/old_in_pure_postcondition.rs
@@ -1,21 +1,17 @@
 use prusti_contracts::*;
 
-#[extern_spec]
-impl<T> std::option::Option<T> {
-    #[pure] // <=== Error triggered by this
-    #[requires(self.is_some())]
-    #[ensures(old(self) === Some(result))]
-    pub fn unwrap(self) -> T; //~ ERROR old expressions should not appear in the postconditions of pure functions
+struct MyWrapper(u32);
 
+impl MyWrapper {
     #[pure]
-    #[ensures(result == matches!(self, Some(_)))]
-    pub const fn is_some(&self) -> bool;
+    #[ensures(old(self.0) == self.0)]
+    fn unwrap(&self) -> u32 { //~ ERROR old expressions should not appear in the postconditions of pure functions
+        self.0
+    }
 }
 
-#[pure]
-#[requires(x.is_some())]
-fn test(x: Option<i32>) -> i32 {
-    // Following error is due to stub encoding of invalid external spec for function `unwrap()`
+fn test(x: &MyWrapper) -> u32 {
+    // Following error is due to stub encoding of invalid spec for function `unwrap()`
     x.unwrap() //~ ERROR precondition of pure function call might not hold
 }
 
diff --git a/prusti-tests/tests/verify/fail/incorrect/old_in_pure_postcondition_extern.rs b/prusti-tests/tests/verify/fail/incorrect/old_in_pure_postcondition_extern.rs
new file mode 100644
index 00000000000..01faa27f922
--- /dev/null
+++ b/prusti-tests/tests/verify/fail/incorrect/old_in_pure_postcondition_extern.rs
@@ -0,0 +1,22 @@
+use prusti_contracts::*;
+
+#[extern_spec]
+impl<T> std::option::Option<T> {
+    #[pure] // <=== Error triggered by this
+    #[requires(self.is_some())]
+    #[ensures(old(self) === Some(result))]
+    pub fn unwrap(self) -> T; //~ ERROR old expressions should not appear in the postconditions of pure functions
+
+    #[pure]
+    #[ensures(result == matches!(self, Some(_)))]
+    pub const fn is_some(&self) -> bool;
+}
+
+#[pure]
+#[requires(x.is_some())]
+fn test(x: Option<i32>) -> i32 {
+    // Following error is due to stub encoding of invalid external spec for function `unwrap()`
+    x.unwrap() //~ ERROR precondition of pure function call might not hold
+}
+
+fn main() { }