-
Notifications
You must be signed in to change notification settings - Fork 89
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Harness Output in Individual Files #3356
Comments
Thank you for the feature request! This is a great idea for an improvement. Can you describe a little bit more about how this would be useful for a user in a project, if possible? |
Hi @jaisnan, for a project our team is working on we wanted the capability to use Kani in a CD/CI capacity, and provide information about the run in a quick easy interface. Having to manually parse the single large output file seems more difficult than having the option of having individual harnesses output into files which can then be managed. |
I have a test version of what it could look like but I'm not sure if this is how you guys would want to do it: if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
let file_name = String::from("./kani-harness-result/".to_owned() + &harness.pretty_name.clone());
let path = Path::new(&file_name);
let prefix = path.parent().unwrap();
std::fs::create_dir_all(prefix).unwrap();
let file = File::create(file_name.clone());
let output = result.render(
&self.args.output_format,
harness.attributes.should_panic,
self.args.coverage,
);
if let Err(e) = writeln!(file.unwrap(), "{}", output) {
eprintln!("Failed to write to file {}: {}", file_name, e);
}
println!("{}", output);
} Basically it makes a directory structure based on the harness names and then puts the output of a harness into a single file based on its name. |
Of course! We encourage and welcome external pull requests! Please feel free to add your changes as a PR. |
I really like this idea. In fact, I would suggest that this should be done whenever the terse output is selected (which I think should be the default one). In this case, Kani could print the verification summary and save detailed result in a file, like you mentioned. One feedback for your potential patch is to use the target directory as the base directory of your new result directory. |
Requested feature: Harness Output in Individual Files
Use case: Easily parse output by having each harness output be an a unique file.
Printing is done to the std output but having each harness output be in a file helps with parsing. Possibly files named based on harness name.
This is currently done in each harness here in kani-driver line 124:
The text was updated successfully, but these errors were encountered: