user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

tweak genmc error report note

Browse source
This commit is contained in:
Ralf Jung 2025-09-18 20:41:06 +02:00
parent 2c1f1f0e9b
commit 00bfe9ce6e
10 changed files with 23 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/tools/miri/src/concurrency/genmc/run.rs
View file

@ -70,7 +70,7 @@ fn run_genmc_mode_impl<'tcx>(
// Execute the program until completion to get the return value, or return if an error happens:
let Some(return_code) = eval_entry(genmc_ctx.clone()) else {
genmc_ctx.print_genmc_output(genmc_config);
genmc_ctx.print_genmc_output(genmc_config, tcx);
return None;
};
@ -97,7 +97,7 @@ fn run_genmc_mode_impl<'tcx>(
// Since we don't have any span information for the error at this point,
// we just print GenMC's error string, and the full GenMC output if requested.
eprintln!("(GenMC) Error detected: {error}");
genmc_ctx.print_genmc_output(genmc_config);
genmc_ctx.print_genmc_output(genmc_config, tcx);
return None;
}
}
@ -110,13 +110,13 @@ impl GenmcCtx {
///
/// This message can be very verbose and is likely not useful for the average user.
/// This function should be called *after* Miri has printed all of its output.
fn print_genmc_output(&self, genmc_config: &GenmcConfig) {
fn print_genmc_output(&self, genmc_config: &GenmcConfig, tcx: TyCtxt<'_>) {
if genmc_config.print_genmc_output {
eprintln!("GenMC error report:");
eprintln!("{}", self.get_result_message());
} else {
eprintln!(
"(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)"
tcx.dcx().note(
"add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report"
);
}
}

3
src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr
View file

@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
LL | f();
| ^^^
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error

3
src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rel_rlx.stderr
View file

@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
LL | f();
| ^^^
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error

3
src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_acq.stderr
View file

@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
LL | f();
| ^^^
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error

3
src/tools/miri/tests/genmc/fail/data_race/weak_orderings.rlx_rlx.stderr
View file

@ -16,6 +16,7 @@ note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/f
LL | f();
| ^^^
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error

3
src/tools/miri/tests/genmc/fail/loom/buggy_inc.stderr
View file

@ -10,6 +10,7 @@ LL | std::process::abort();
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error

3
src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr
View file

@ -10,6 +10,7 @@ LL | std::process::abort();
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error

3
src/tools/miri/tests/genmc/fail/simple/2w2w_weak.relaxed4.stderr
View file

@ -10,6 +10,7 @@ LL | std::process::abort();
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error

3
src/tools/miri/tests/genmc/fail/simple/2w2w_weak.release4.stderr
View file

@ -10,6 +10,7 @@ LL | std::process::abort();
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error

3
src/tools/miri/tests/genmc/fail/simple/2w2w_weak.sc3_rel1.stderr
View file

@ -10,6 +10,7 @@ LL | std::process::abort();
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
(Add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report.)
note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
error: aborting due to 1 previous error