Skip to content

Commit

Permalink
Append harness name to the graph file
Browse files Browse the repository at this point in the history
Our debug feature that dumps the call graph into a file was using the
crate name, which meant that the call graph kept getting overriden.

Instead, append the name of the harness to the file.
  • Loading branch information
celinval committed Sep 19, 2024
1 parent cda1b30 commit a0e6d59
Showing 1 changed file with 9 additions and 3 deletions.
12 changes: 9 additions & 3 deletions kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ pub fn collect_reachable_items(
#[cfg(debug_assertions)]
collector
.call_graph
.dump_dot(tcx)
.dump_dot(tcx, starting_points.first().cloned())
.unwrap_or_else(|e| tracing::error!("Failed to dump call graph: {e}"));

tcx.dcx().abort_if_errors();
Expand Down Expand Up @@ -579,12 +579,18 @@ impl CallGraph {

/// Print the graph in DOT format to a file.
/// See <https://graphviz.org/doc/info/lang.html> for more information.
fn dump_dot(&self, tcx: TyCtxt) -> std::io::Result<()> {
fn dump_dot(&self, tcx: TyCtxt, initial: Option<MonoItem>) -> std::io::Result<()> {
if let Ok(target) = std::env::var("KANI_REACH_DEBUG") {
debug!(?target, "dump_dot");
let name = initial.map(|item| Node(item).to_string()).unwrap_or_default();
let outputs = tcx.output_filenames(());
let base_path = outputs.path(OutputType::Metadata);
let path = base_path.as_path().with_extension("dot");
let file_stem = format!(
"{}_{}.dot",
base_path.as_path().file_stem().unwrap().to_string_lossy(),
name
);
let path = base_path.as_path().parent().unwrap().join(file_stem);
let out_file = File::create(path)?;
let mut writer = BufWriter::new(out_file);
writeln!(writer, "digraph ReachabilityGraph {{")?;
Expand Down

0 comments on commit a0e6d59

Please sign in to comment.