Skip to content

Commit

Permalink
Emit some suggestions when CBMC runs out of memory
Browse files Browse the repository at this point in the history
  • Loading branch information
JustusAdam committed Nov 19, 2023
1 parent 4066a23 commit 564afa9
Showing 1 changed file with 10 additions and 1 deletion.
11 changes: 10 additions & 1 deletion kani-driver/src/call_cbmc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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}",
)
}
}
Expand Down

0 comments on commit 564afa9

Please sign in to comment.