Report results as UNDETERMINED instead of SUCCESS if an unwinding ass…

…ertion fails (#889)

scripts/cbmc_json_parser.py

@@ -205,15 +205,14 @@ def postprocess_results(properties):
     annotate_properties_with_reach_results(properties, reach_checks)
 
     for property in properties:
-        if has_reachable_unsupported_constructs:
+        if has_reachable_unsupported_constructs or has_failed_unwinding_asserts:
             # Change SUCCESS to UNDETERMINED for all properties
             if property["status"] == "SUCCESS":
                 property["status"] = "UNDETERMINED"
         elif GlobalMessages.REACH_CHECK_KEY in property and property[GlobalMessages.REACH_CHECK_KEY] == "SUCCESS":
             # Change SUCCESS to UNREACHABLE
             assert property["status"] == "SUCCESS", "** ERROR: Expecting an unreachable property to have a status of \"SUCCESS\""
             property["status"] = "UNREACHABLE"
-        # TODO: Handle unwinding assertion failure
 
     messages = ""
     if has_reachable_unsupported_constructs:

tests/expected/report/insufficient_unwind/expected

@@ -0,0 +1,3 @@
+UNDETERMINED
+[Kani] info: Verification output shows one or more unwinding failures.
+[Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.

tests/expected/report/insufficient_unwind/test.rs

@@ -0,0 +1,18 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that Kani reports UNDETERMINED if the specified unwinding is
+// insufficient. The minimum required unwinding is 7.
+
+// kani-flags: --unwind 6
+
+fn main() {
+    let x: bool = kani::any();
+    let v = if x { vec![1, 2, 3] } else { vec![1, 1, 1, 1, 1, 1] };
+
+    let mut sum = 0;
+    for i in v {
+        sum += i;
+    }
+    assert!(sum == 6);
+}

tests/expected/unwind_tip/expected

@@ -1,2 +1,3 @@
+UNDETERMINED
 [Kani] info: Verification output shows one or more unwinding failures.
 [Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.