diff --git a/scripts/cbmc_json_parser.py b/scripts/cbmc_json_parser.py index 955d83031145..9a0d58387f04 100755 --- a/scripts/cbmc_json_parser.py +++ b/scripts/cbmc_json_parser.py @@ -205,7 +205,7 @@ 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" @@ -213,7 +213,6 @@ def postprocess_results(properties): # 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: diff --git a/tests/expected/report/insufficient_unwind/expected b/tests/expected/report/insufficient_unwind/expected new file mode 100644 index 000000000000..5dd5d65f0953 --- /dev/null +++ b/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`. diff --git a/tests/expected/report/insufficient_unwind/test.rs b/tests/expected/report/insufficient_unwind/test.rs new file mode 100644 index 000000000000..32921baea6f4 --- /dev/null +++ b/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); +} diff --git a/tests/expected/unwind_tip/expected b/tests/expected/unwind_tip/expected index cb7e4f45d9a0..5dd5d65f0953 100644 --- a/tests/expected/unwind_tip/expected +++ b/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`.