Skip to content

Commit b0301a3

Browse files
authored
Emit suggestions and an explanation when CBMC runs out of memory (rust-lang#2885)
Improves the error reported to the user when the system kills CBMC to reclaim memory. Resolves rust-lang#2715
1 parent 4066a23 commit b0301a3

File tree

1 file changed

+10
-1
lines changed

1 file changed

+10
-1
lines changed

kani-driver/src/call_cbmc.rs

+10-1
Original file line numberDiff line numberDiff line change
@@ -327,8 +327,17 @@ impl VerificationResult {
327327
}
328328
Err(exit_status) => {
329329
let verification_result = console::style("FAILED").red();
330+
let explanation = if *exit_status == 137 {
331+
"CBMC appears to have run out of memory. You may want to rerun your proof in \
332+
an environment with additional memory or use stubbing to reduce the size of the \
333+
code the verifier reasons about.\n"
334+
} else {
335+
""
336+
};
330337
format!(
331-
"\nCBMC failed with status {exit_status}\nVERIFICATION:- {verification_result}\n",
338+
"\nCBMC failed with status {exit_status}\n\
339+
VERIFICATION:- {verification_result}\n\
340+
{explanation}",
332341
)
333342
}
334343
}

0 commit comments

Comments
 (0)