Add double-attr-invariant test

tests/ui/attr-invariant/double-attr-invariant/double-attr-invariant.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that there is a compilation error when the predicate passed to
+//! `kani::invariant` attribute would result in a compiler error.
+
+extern crate kani;
+use kani::Invariant;
+
+// Note: The struct fields `x` and `y` are references in this context, we should
+// refer to `*x` and `*y` instead.
+#[kani::invariant(*x >= 0)]
+#[kani::invariant(*y >= 0)]
+struct Point {
+ x: i32,
+ y: i32,
+}

tests/ui/attr-invariant/double-attr-invariant/expected

@@ -0,0 +1,6 @@
+error[E0119]: conflicting implementations of trait `kani::Invariant` for type `Point`
+ |
+12 | #[kani::invariant(*x >= 0)]
+ | --------------------------- first implementation here
+13 | #[kani::invariant(*y >= 0)]
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `Point`