Add more tests and do some renames

tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute automatically generates
+//! the `Arbitrary` implementation, and also that the values it generates
+//! respect the type invariant.
+
+//! In this case, we test the attribute on a struct with a generic type `T`
+//! which requires the bound `From<i32>` because of the comparisons in the
+//! `#[safety_constraint(...)]` predicate. The struct represents an abstract
+//! value for which we only track its sign. The actual value is kept private.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+#[safety_constraint((*positive && *conc_value >= 0.into()) || (!*positive && *conc_value < 0.into()))]
+struct AbstractValue<T>
+where
+    T: PartialOrd + From<i32>,
+{
+    pub positive: bool,
+    conc_value: T,
+}
+
+#[kani::proof]
+fn check_abstract_value() {
+    let value: AbstractValue<i32> = kani::any();
+    assert!(value.is_safe());
+}

tests/expected/safety-constraint-attribute/abstract-value/expected

@@ -0,0 +1,7 @@
+Check 1: check_abstract_value.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: value.is_safe()"
+
+VERIFICATION:- SUCCESSFUL
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/expected/attr-invariant/check_invariant/check_invariant.rs → tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs

@@ -9,14 +9,19 @@ use kani::Invariant;
 
 #[derive(kani::Arbitrary)]
 #[derive(kani::Invariant)]
-#[safety_constraint(true)]
-struct Point {
+#[safety_constraint(*x == *y)]
+struct SameCoordsPoint {
     x: i32,
     y: i32,
 }
 
 #[kani::proof]
 fn check_invariant() {
-    let point: Point = kani::any();
+    let point: SameCoordsPoint = kani::any();
     assert!(point.is_safe());
+
+    // Assuming `point.x != point.y` here should be like assuming `false`.
+    // The assertion should be unreachable because we're blocking the path.
+    kani::assume(point.x != point.y);
+    assert!(false, "this assertion should unreachable");
 }

tests/expected/safety-constraint-attribute/check-invariant/expected

@@ -0,0 +1,7 @@
+Check 1: check_invariant.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: point.is_safe()"
+
+Check 2: check_invariant.assertion.2\
+         - Status: UNREACHABLE\
+         - Description: ""this is unreachable""

tests/expected/safety-constraint-attribute/grade-example/expected

@@ -0,0 +1,11 @@
+Check 4: Grade::check_percentage_safety.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: self.percentage <= 100"
+
+Check 5: check_grade_safe.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: grade.is_safe()"
+
+VERIFICATION:- SUCCESSFUL
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/expected/safety-constraint-attribute/grade-example/grade-example.rs

@@ -0,0 +1,44 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute automatically generates
+//! the `Arbitrary` implementation, and also that the values it generates
+//! respect the type invariant.
+
+//! In this case, we test the attribute on a struct that represents a hybrid
+//! grade (letter-numerical) which should keep the following equivalences:
+//!  - A for 90-100%
+//!  - B for 80-89%
+//!  - C for 70-79%
+//!  - D for 60-69%
+//!  - F for 0-59%
+//!
+//! In addition, we explicitly test that `percentage` is 0-100%
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+#[safety_constraint((*letter == 'A' && *percentage >= 90 && *percentage <= 100) ||
+                    (*letter == 'B' && *percentage >= 80 && *percentage < 90) ||
+                    (*letter == 'C' && *percentage >= 70 && *percentage < 80) ||
+                    (*letter == 'D' && *percentage >= 60 && *percentage < 70) ||
+                    (*letter == 'F' && *percentage < 60))]
+struct Grade {
+    letter: char,
+    percentage: u32,
+}
+
+impl Grade {
+    pub fn check_percentage_safety(&self) {
+        assert!(self.percentage <= 100);
+    }
+}
+
+#[kani::proof]
+fn check_grade_safe() {
+    let grade: Grade = kani::any();
+    assert!(grade.is_safe());
+    grade.check_percentage_safety();
+}