From 564afa953a65bbe8085a29f2ba460f36e05708dd Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Sat, 18 Nov 2023 23:11:02 -0500 Subject: [PATCH 1/2] Emit some suggestions when CBMC runs out of memory --- kani-driver/src/call_cbmc.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 37f66a9f38ad..bdd18545a9ef 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -327,8 +327,17 @@ impl VerificationResult { } Err(exit_status) => { let verification_result = console::style("FAILED").red(); + let explanation = if exit_status == 137 { + "CBMC appears to have run out of memory. You may want to rerun your proof in \ + an environment with additional memory or use stubbing to reduce the size of the \ + code the verifier reasons about.\n" + } else { + "" + }; format!( - "\nCBMC failed with status {exit_status}\nVERIFICATION:- {verification_result}\n", + "\nCBMC failed with status {exit_status}\n\ + VERIFICATION:- {verification_result}\n\ + {explanation}", ) } } From cb53939e9b348ae50978f99c09d2b8cada70e47b Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Sun, 19 Nov 2023 11:05:10 -0500 Subject: [PATCH 2/2] Compile error --- kani-driver/src/call_cbmc.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index bdd18545a9ef..a806331401cd 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -327,7 +327,7 @@ impl VerificationResult { } Err(exit_status) => { let verification_result = console::style("FAILED").red(); - let explanation = if exit_status == 137 { + let explanation = if *exit_status == 137 { "CBMC appears to have run out of memory. You may want to rerun your proof in \ an environment with additional memory or use stubbing to reduce the size of the \ code the verifier reasons about.\n"