Filter sanity checks (model-checking#1146)

Properties which are sanity checks needed to be removed from the UI. They are now marked with the property_class "sanity_check" which makes it easy to filter such checks out as the pipeline to add, remove and edit checks based on their property_class has already been setup.

scripts/cbmc_json_parser.py

@@ -329,6 +329,7 @@ def postprocess_results(properties, extra_ptr_check):
     has_failed_unwinding_asserts = has_check_failure(properties, GlobalMessages.UNWINDING_ASSERT_DESC)
     has_reachable_undefined_functions = modify_undefined_function_checks(properties)
     properties, reach_checks = filter_reach_checks(properties)
+    properties = filter_sanity_checks(properties)
     annotate_properties_with_reach_results(properties, reach_checks)
     remove_check_ids_from_description(properties)
 
@@ -369,10 +370,22 @@ def has_check_failure(properties, message):
             return True
     return False
 
-
 def filter_reach_checks(properties):
     return filter_properties(properties, GlobalMessages.REACH_CHECK_DESC)
 
+def filter_sanity_checks(properties):
+    """
+    Specific filter for sanity_check checks that removed checks with SUCCESS status
+    """
+    filtered_properties = []
+    property_class = "sanity_check"
+    for property in properties:
+        if property_class in extract_property_class(property) and property["status"] == "SUCCESS":
+            pass
+        else:
+            filtered_properties.append(property)
+
+    return filtered_properties
 
 def filter_properties(properties, message):
     """

tests/ui/filter-sanity-checks/expected

@@ -0,0 +1,3 @@
+sanity_check.1\
+Status: FAILURE\
+Description: "Reached assignment statement with unequal types Pointer { typ: StructTag("tag-Unit") } StructTag("tag-Unit")"

tests/ui/filter-sanity-checks/sanity_check_fail.rs

@@ -0,0 +1,38 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+/// This testcase is currently failing with the following error:
+///
+/// [assertion.2] Reached assignment statement with unequal types Pointer { typ:
+/// StructTag("tag-Unit") } Pointer { typ: StructTag("tag-_3943305294634710273") }: FAILURE
+///
+/// If you run:
+/// ```
+/// RUSTFLAGS="--cfg=ok" kani fixme_niche_opt.rs
+/// ```
+/// This test will succeed.
+///
+/// Issue: https://github.com/model-checking/kani/issues/729
+
+enum Error {
+    Error1,
+    Error2,
+}
+
+/// This version fails.
+#[cfg(not(ok))]
+fn to_option<T: Copy, E>(result: &Result<T, E>) -> Option<T> {
+    if let Ok(v) = result { Some(*v) } else { None }
+}
+
+/// This version succeeds.
+#[cfg(ok)]
+fn to_option<T: Copy, E>(result: &Result<T, E>) -> Option<T> {
+    if let Ok(v) = *result { Some(v) } else { None }
+}
+
+#[kani::proof]
+fn main() {
+    let result: Result<(), Error> = Ok(());
+    assert!(to_option(&result).is_some());
+}