From 1a3e2a6a811a42103b2369f4b1dab94decc6138e Mon Sep 17 00:00:00 2001 From: Rajath Kotyal Date: Wed, 26 Feb 2025 16:27:02 -0800 Subject: [PATCH] set kani default value to 1, added test_case --- kani-driver/src/call_cbmc.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 92c82f25888d..5623786aa946 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -544,7 +544,8 @@ pub fn resolve_unwind_value( ) -> Option { // Check for which flag is being passed and prioritize extracting unwind from the // respective flag/annotation. - args.unwind.or(harness_metadata.attributes.unwind_value).or(args.default_unwind) + // If no unwind value is specified, default to 1 to prevent memory consumption issues + args.unwind.or(harness_metadata.attributes.unwind_value).or(args.default_unwind).or(Some(1)) } #[cfg(test)] @@ -575,7 +576,7 @@ mod tests { } // test against no unwind annotation - assert_eq!(resolve(&args_empty, &harness_none), None); + assert_eq!(resolve(&args_empty, &harness_none), Some(1)); assert_eq!(resolve(&args_only_default, &harness_none), Some(2)); assert_eq!(resolve(&args_only_harness, &harness_none), Some(1)); assert_eq!(resolve(&args_both, &harness_none), Some(1));