Skip to content

Commit

Permalink
Fix helper pick-up and rename tests
Browse files Browse the repository at this point in the history
  • Loading branch information
adpaco-aws committed Jul 18, 2024
1 parent b6ec5b9 commit c3fc474
Show file tree
Hide file tree
Showing 15 changed files with 10 additions and 10 deletions.
4 changes: 2 additions & 2 deletions library/kani_macros/src/derive.rs
Original file line number Diff line number Diff line change
Expand Up @@ -240,12 +240,12 @@ fn parse_inv_expr(ident: &Ident, field: &syn::Field) -> Option<TokenStream> {

// Keep the helper attribute if we find it
for attr in &field.attrs {
if attr.path().is_ident("invariant") {
if attr.path().is_ident("safety_constraint") {
inv_helper_attr = Some(attr);
}
}

// Parse the arguments in the invariant helper attribute
// Parse the arguments in the `#[safety_constraint(...)]` attribute
if let Some(attr) = inv_helper_attr {
let expr_args: Result<syn::Expr, syn::Error> = attr.parse_args();

Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! Check that the invariant attribute helper adds the conditions provided to
//! Check that the `#[safety_constraint(...)]` attribute helper adds the conditions provided to
//! the attribute to the derived `Arbitrary` implementation.
extern crate kani;
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! Check that the invariant attribute helper adds the conditions provided to
//! Check that the `#[safety_constraint(...)]` attribute helper adds the conditions provided to
//! the attribute to the derived `Invariant` implementation.
extern crate kani;
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! Check that functions can be called in the invariant attribute helpers.
//! Check that functions can be called in the `#[safety_constraint(...)]` attribute helpers.
//! This is like the `invariant_helper` test but using a function instead
//! of passing in a predicate.
Expand Down
2 changes: 1 addition & 1 deletion tests/ui/derive-invariant/helper-empty/helper-empty.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! Check the compilation error for the invariant attribute helper when an
//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when an
//! argument isn't provided.
extern crate kani;
Expand Down
2 changes: 1 addition & 1 deletion tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! Check the compilation error for the invariant attribute helper when the
//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when the
//! argument is not a proper expression.
extern crate kani;
Expand Down
4 changes: 2 additions & 2 deletions tests/ui/derive-invariant/helper-wrong-expr/expected
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
error[E0308]: mismatched types
|
14 | #[safety_constraint(x >= 0)]
| ^ expected `&i32`, found integer
| ^ expected `&i32`, found integer
|
help: consider dereferencing the borrow
|
14 | #[safety_constraint(*x >= 0)]
| +
|
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! Check the compilation error for the invariant attribute helper when the
//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when the
//! argument cannot be evaluated in the struct's context.
extern crate kani;
Expand Down

0 comments on commit c3fc474

Please sign in to comment.