Add unwind tip to CBMC result parser script

scripts/cbmc_json_parser.py

@@ -220,6 +220,9 @@ def postprocess_results(properties):
         messages += "** WARNING: A Rust construct that is not currently supported " \
                     "by Kani was found to be reachable. Check the results for " \
                     "more details."
+    if has_failed_unwinding_asserts:
+        messages += "[Kani] info: Verification output shows one or more unwinding failures.\n" \
+                    "[Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.\n"
 
     return properties, messages
 

tests/expected/unwind_tip/expected

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

tests/expected/unwind_tip/main.rs

@@ -0,0 +1,27 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// cbmc-flags: --unwind 9
+
+// This example is a copy of the `cbmc` test in
+// `src/test/kani/LoopLoop_NonReturning/main_no_unwind_asserts.rs`
+//
+// The verification output should show an unwinding assertion failure.
+//
+// In this test, we check that Kani warns the user about unwinding failures
+// and makes a recommendation to fix the issue.
+fn main() {
+    let mut a: u32 = kani::any();
+
+    if a < 1024 {
+        loop {
+            a = a / 2;
+
+            if a == 0 {
+                break;
+            }
+        }
+
+        assert!(a == 0);
+    }
+}