Merge branch 'main' into toolchain-2023-11-12

model-checking · Nov 20, 2023 · 269bea8 · 269bea8
2 parents 79220e5 + b0301a3
commit 269bea8
Showing 1 changed file with 10 additions and 1 deletion.
diff --git 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}",
                 )
             }
         }