From 42b415c7899047a29426bb1185002fca48b926a2 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Tue, 9 Jul 2024 20:29:10 +0000
Subject: [PATCH] Fix invalid-pred-error test.

---
 .../invalid-pred-error/expected               | 26 +++++++++----------
 .../invalid-pred-error/invalid-pred-error.rs  |  6 ++---
 2 files changed, 15 insertions(+), 17 deletions(-)

diff --git a/tests/ui/attr-invariant/invalid-pred-error/expected b/tests/ui/attr-invariant/invalid-pred-error/expected
index 73f030c4cae8..61af20fea348 100644
--- a/tests/ui/attr-invariant/invalid-pred-error/expected
+++ b/tests/ui/attr-invariant/invalid-pred-error/expected
@@ -1,21 +1,19 @@
-error[E0425]: cannot find value `x` in this scope
-  --> invalid-pred-error.rs:10:19
+error[E0308]: mismatched types
    |
-10 | #[kani::invariant(x.is_safe() && y.is_safe())]
-   |                   ^
+13 | #[kani::invariant(x >= 0 && y >= 0)]
+   |                        ^ expected `&i32`, found integer
    |
-help: you might have meant to use the available field
+help: consider dereferencing the borrow
    |
-10 | #[kani::invariant(self.x.is_safe() && y.is_safe())]
-   |                   +++++
+13 | #[kani::invariant(*x >= 0 && y >= 0)]
+   |                   +
 
-error[E0425]: cannot find value `y` in this scope
-  --> invalid-pred-error.rs:10:34
+error[E0308]: mismatched types
    |
-10 | #[kani::invariant(x.is_safe() && y.is_safe())]
-   |                                  ^
+13 | #[kani::invariant(x >= 0 && y >= 0)]
+   |                                  ^ expected `&i32`, found integer
    |
-help: you might have meant to use the available field
+help: consider dereferencing the borrow
+   |
+13 | #[kani::invariant(x >= 0 && *y >= 0)]
    |
-10 | #[kani::invariant(x.is_safe() && self.y.is_safe())]
-   |                                  +++++
diff --git a/tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs b/tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs
index 0c69b7e76eb3..e1aaf6e7da91 100644
--- a/tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs
+++ b/tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs
@@ -7,10 +7,10 @@
 extern crate kani;
 use kani::Invariant;
 
-// Note: The `x.is_safe() && y.is_safe()` requires `self` before each struct
-// field to be evaluated in the `is_safe` function body.
+// Note: The struct fields `x` and `y` are references in this context, we should
+// refer to `*x` and `*y` instead.
 #[derive(kani::Arbitrary)]
-#[kani::invariant(x.is_safe() && y.is_safe())]
+#[kani::invariant(x >= 0 && y >= 0)]
 struct Point {
     x: i32,
     y: i32,