Update comments so they're clear.

adpaco-aws · Jul 22, 2024 · 477d9bf · 477d9bf
1 parent 2e7c94c
commit 477d9bf
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 8 deletions.
diff --git a/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs
@@ -25,16 +25,17 @@ fn check_invariant_helper_ok() {
 #[kani::proof]
 #[kani::should_panic]
 fn check_invariant_helper_fail() {
-    // In this case, `kani::any()` returns unconstrained values that don't
-    // respect the invariants.
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints.
     let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
     assert!(pos_point.is_safe());
 }
 
 #[kani::proof]
 fn check_invariant_helper_ok_manual() {
-    // In this case, `kani::any()` returns unconstrained values that don't
-    // respect the invariants. However, we manually constrain them later.
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints. However, we
+    // manually constrain them later.
     let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
     kani::assume(pos_point.x >= 0);
     kani::assume(pos_point.y >= 0);

diff --git a/.../expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs b/.../expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs
@@ -30,16 +30,17 @@ fn check_invariant_helper_ok() {
 #[kani::proof]
 #[kani::should_panic]
 fn check_invariant_helper_fail() {
-    // In this case, `kani::any()` returns unconstrained values that don't
-    // respect the invariants.
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints.
     let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
     assert!(pos_point.is_safe());
 }
 
 #[kani::proof]
 fn check_invariant_helper_ok_manual() {
-    // In this case, `kani::any()` returns unconstrained values that don't
-    // respect the invariants. However, we manually constrain them later.
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints. However, we
+    // manually constrain them later.
     let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
     kani::assume(pos_point.x >= 0);
     kani::assume(pos_point.y >= 0);