From c3fc474ca839c782b73226b7d10e320d98907146 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 18 Jul 2024 15:25:03 +0000 Subject: [PATCH] Fix helper pick-up and rename tests --- library/kani_macros/src/derive.rs | 4 ++-- .../{invariant_helper => safety_constraint_helper}/expected | 0 .../safety_constraint_helper.rs} | 2 +- .../{invariant_helper => safety_constraint_helper}/expected | 0 .../safety_constraint_helper.rs} | 2 +- .../expected | 0 .../safety_constraint_helper_funs.rs} | 2 +- .../{invariant_fail => safety_invariant_fail}/expected | 0 .../safety_invariant_fail.rs} | 0 .../expected | 0 .../safety_invariant_fail_mut.rs} | 0 tests/ui/derive-invariant/helper-empty/helper-empty.rs | 2 +- tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs | 2 +- tests/ui/derive-invariant/helper-wrong-expr/expected | 4 ++-- .../derive-invariant/helper-wrong-expr/helper-wrong-expr.rs | 2 +- 15 files changed, 10 insertions(+), 10 deletions(-) rename tests/expected/derive-arbitrary/{invariant_helper => safety_constraint_helper}/expected (100%) rename tests/expected/derive-arbitrary/{invariant_helper/invariant_helper.rs => safety_constraint_helper/safety_constraint_helper.rs} (88%) rename tests/expected/derive-invariant/{invariant_helper => safety_constraint_helper}/expected (100%) rename tests/expected/derive-invariant/{invariant_helper/invariant_helper.rs => safety_constraint_helper/safety_constraint_helper.rs} (92%) rename tests/expected/derive-invariant/{invariant_helper_funs => safety_constraint_helper_funs}/expected (100%) rename tests/expected/derive-invariant/{invariant_helper_funs/invariant_helper_funs.rs => safety_constraint_helper_funs/safety_constraint_helper_funs.rs} (93%) rename tests/expected/derive-invariant/{invariant_fail => safety_invariant_fail}/expected (100%) rename tests/expected/derive-invariant/{invariant_fail/invariant_fail.rs => safety_invariant_fail/safety_invariant_fail.rs} (100%) rename tests/expected/derive-invariant/{invariant_fail_mut => safety_invariant_fail_mut}/expected (100%) rename tests/expected/derive-invariant/{invariant_fail_mut/invariant_fail_mut.rs => safety_invariant_fail_mut/safety_invariant_fail_mut.rs} (100%) diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 6962eecc0040..3e41100fd810 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -240,12 +240,12 @@ fn parse_inv_expr(ident: &Ident, field: &syn::Field) -> Option { // 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 = attr.parse_args(); diff --git a/tests/expected/derive-arbitrary/invariant_helper/expected b/tests/expected/derive-arbitrary/safety_constraint_helper/expected similarity index 100% rename from tests/expected/derive-arbitrary/invariant_helper/expected rename to tests/expected/derive-arbitrary/safety_constraint_helper/expected diff --git a/tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs b/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs similarity index 88% rename from tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs rename to tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs index 101b25d1f781..5b608aa2a3c0 100644 --- a/tests/expected/derive-arbitrary/invariant_helper/invariant_helper.rs +++ b/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs @@ -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; diff --git a/tests/expected/derive-invariant/invariant_helper/expected b/tests/expected/derive-invariant/safety_constraint_helper/expected similarity index 100% rename from tests/expected/derive-invariant/invariant_helper/expected rename to tests/expected/derive-invariant/safety_constraint_helper/expected diff --git a/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs similarity index 92% rename from tests/expected/derive-invariant/invariant_helper/invariant_helper.rs rename to tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs index 1ac380335b8b..d824a706c8b8 100644 --- a/tests/expected/derive-invariant/invariant_helper/invariant_helper.rs +++ b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs @@ -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; diff --git a/tests/expected/derive-invariant/invariant_helper_funs/expected b/tests/expected/derive-invariant/safety_constraint_helper_funs/expected similarity index 100% rename from tests/expected/derive-invariant/invariant_helper_funs/expected rename to tests/expected/derive-invariant/safety_constraint_helper_funs/expected diff --git a/tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs similarity index 93% rename from tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs rename to tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs index 50419a206825..cc0132273e80 100644 --- a/tests/expected/derive-invariant/invariant_helper_funs/invariant_helper_funs.rs +++ b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs @@ -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. diff --git a/tests/expected/derive-invariant/invariant_fail/expected b/tests/expected/derive-invariant/safety_invariant_fail/expected similarity index 100% rename from tests/expected/derive-invariant/invariant_fail/expected rename to tests/expected/derive-invariant/safety_invariant_fail/expected diff --git a/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs b/tests/expected/derive-invariant/safety_invariant_fail/safety_invariant_fail.rs similarity index 100% rename from tests/expected/derive-invariant/invariant_fail/invariant_fail.rs rename to tests/expected/derive-invariant/safety_invariant_fail/safety_invariant_fail.rs diff --git a/tests/expected/derive-invariant/invariant_fail_mut/expected b/tests/expected/derive-invariant/safety_invariant_fail_mut/expected similarity index 100% rename from tests/expected/derive-invariant/invariant_fail_mut/expected rename to tests/expected/derive-invariant/safety_invariant_fail_mut/expected diff --git a/tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs b/tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs similarity index 100% rename from tests/expected/derive-invariant/invariant_fail_mut/invariant_fail_mut.rs rename to tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs diff --git a/tests/ui/derive-invariant/helper-empty/helper-empty.rs b/tests/ui/derive-invariant/helper-empty/helper-empty.rs index 1072f72d07ba..3086603cf5db 100644 --- a/tests/ui/derive-invariant/helper-empty/helper-empty.rs +++ b/tests/ui/derive-invariant/helper-empty/helper-empty.rs @@ -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; diff --git a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs index 916b047b7274..080c94371257 100644 --- a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs +++ b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs @@ -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; diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected index efa29c758637..7d14cb1e753a 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/expected +++ b/tests/ui/derive-invariant/helper-wrong-expr/expected @@ -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)] - | + + | diff --git a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs index ed179145c7cb..66b42e02fd68 100644 --- a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs +++ b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs @@ -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;