From b0301a3f4b48b95381de290f370e45b137e3fec5 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Mon, 20 Nov 2023 13:45:44 -0500 Subject: [PATCH] Emit suggestions and an explanation when CBMC runs out of memory (#2885) Improves the error reported to the user when the system kills CBMC to reclaim memory. Resolves #2715 --- 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..a806331401cd 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}", ) } }