Skip to content

Commit df4f3b6

Browse files
committed
tweak genmc error report note
1 parent 7ef3cd9 commit df4f3b6

10 files changed

+23
-14
lines changed

src/concurrency/genmc/run.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ fn run_genmc_mode_impl<'tcx>(
7070

7171
// Execute the program until completion to get the return value, or return if an error happens:
7272
let Some(return_code) = eval_entry(genmc_ctx.clone()) else {
73-
genmc_ctx.print_genmc_output(genmc_config);
73+
genmc_ctx.print_genmc_output(genmc_config, tcx);
7474
return None;
7575
};
7676

@@ -97,7 +97,7 @@ fn run_genmc_mode_impl<'tcx>(
9797
// Since we don't have any span information for the error at this point,
9898
// we just print GenMC's error string, and the full GenMC output if requested.
9999
eprintln!("(GenMC) Error detected: {error}");
100-
genmc_ctx.print_genmc_output(genmc_config);
100+
genmc_ctx.print_genmc_output(genmc_config, tcx);
101101
return None;
102102
}
103103
}
@@ -110,13 +110,13 @@ impl GenmcCtx {
110110
///
111111
/// This message can be very verbose and is likely not useful for the average user.
112112
/// This function should be called *after* Miri has printed all of its output.
113-
fn print_genmc_output(&self, genmc_config: &GenmcConfig) {
113+
fn print_genmc_output(&self, genmc_config: &GenmcConfig, tcx: TyCtxt<'_>) {
114114
if genmc_config.print_genmc_output {
115115
eprintln!("GenMC error report:");
116116
eprintln!("{}", self.get_result_message());
117117
} else {
118-
eprintln!(
119-
"(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)"
118+
tcx.dcx().note(
119+
"add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report"
120120
);
121121
}
122122
}

tests/genmc/fail/data_race/mpu2_rels_rlx.stderr

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
1616
LL | f();
1717
| ^^^
1818

19-
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
19+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
20+
2021
error: aborting due to 1 previous error
2122

tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
1616
LL | f();
1717
| ^^^
1818

19-
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
19+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
20+
2021
error: aborting due to 1 previous error
2122

tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
1616
LL | f();
1717
| ^^^
1818

19-
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
19+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
20+
2021
error: aborting due to 1 previous error
2122

tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
1616
LL | f();
1717
| ^^^
1818

19-
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
19+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
20+
2021
error: aborting due to 1 previous error
2122

tests/genmc/fail/loom/buggy_inc.stderr

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ LL | std::process::abort();
1010

1111
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
1212

13-
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
13+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
14+
1415
error: aborting due to 1 previous error
1516

tests/genmc/fail/loom/store_buffering.genmc.stderr

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ LL | std::process::abort();
1010

1111
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
1212

13-
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
13+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
14+
1415
error: aborting due to 1 previous error
1516

tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ LL | std::process::abort();
1010

1111
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
1212

13-
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
13+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
14+
1415
error: aborting due to 1 previous error
1516

tests/genmc/fail/simple/2w2w_weak.release4.stderr

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ LL | std::process::abort();
1010

1111
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
1212

13-
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
13+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
14+
1415
error: aborting due to 1 previous error
1516

tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ LL | std::process::abort();
1010

1111
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
1212

13-
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
13+
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
14+
1415
error: aborting due to 1 previous error
1516

0 commit comments

Comments
 (0)