Skip to content

Commit

Permalink
Add side-effect test
Browse files Browse the repository at this point in the history
  • Loading branch information
adpaco-aws committed Jul 22, 2024
1 parent 11e5597 commit 05dea45
Show file tree
Hide file tree
Showing 2 changed files with 32 additions and 0 deletions.
10 changes: 10 additions & 0 deletions tests/ui/derive-invariant/helper-side-effect/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
error[E0596]: cannot borrow `*x` as mutable, as it is behind a `&` reference
--> safety_constraint_helper_side_effect/safety_constraint_helper_side_effect.rs:12:28
|
| #[safety_constraint({*(x.as_mut()) = 0; true})]
| ^ `x` is a `&` reference, so the data it refers to cannot be borrowed as mutable
|
help: consider specifying this binding's type
|
| x: &mut std::boxed::Box<i32>: Box<i32>,
| +++++++++++++++++++++++++++
22 changes: 22 additions & 0 deletions tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! Check that side effect expressions in the `#[safety_constraint(...)]`
//! attribute helpers are not allowed.
extern crate kani;
use kani::Invariant;

#[derive(kani::Arbitrary)]
#[derive(kani::Invariant)]
struct PositivePoint {
#[safety_constraint({*(x.as_mut()) = 0; true})]
x: Box<i32>,
y: i32,
}

#[kani::proof]
fn check_invariant_helper_ok() {
let pos_point: PositivePoint = kani::any();
assert!(pos_point.is_safe());
}

0 comments on commit 05dea45

Please sign in to comment.