Fix comments in all test cases

tests/expected/attr-invariant/check_invariant/check_invariant.rs

@@ -1,7 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! Check that Kani can automatically derive `Invariant` for structs with named fields.
+//! Check that the `kani::invariant` attribute is applied and the associated
+//! invariant can be checked through an `is_safe` call.
 
 extern crate kani;
 use kani::Invariant;

tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs

@@ -1,11 +1,14 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! Check that Kani can automatically derive `Invariant` for structs with named fields.
+//! 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 `x.is_safe() && y.is_safe()` requires `self` before each struct
+// field to be evaluated in the `is_safe` function body.
 #[derive(kani::Arbitrary)]
 #[kani::invariant(x.is_safe() && y.is_safe())]
 struct Point {

tests/ui/attr-invariant/no-struct-error/no-struct-error.rs

@@ -1,7 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! Check that Kani can automatically derive `Invariant` for structs with named fields.
+//! Check that Kani raises an error when the `kani::invariant` attribute is
+//! applied to items which is not a struct.
 
 extern crate kani;
 use kani::Invariant;