Skip to content

Commit

Permalink
Fix invalid-pred-error test.
Browse files Browse the repository at this point in the history
  • Loading branch information
adpaco-aws committed Jul 9, 2024
1 parent dd2206d commit 42b415c
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 17 deletions.
26 changes: 12 additions & 14 deletions tests/ui/attr-invariant/invalid-pred-error/expected
Original file line number Diff line number Diff line change
@@ -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())]
| +++++
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down

0 comments on commit 42b415c

Please sign in to comment.