diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs index 8f563806f..d6f8dc697 100644 --- a/charon/src/bin/charon-driver/main.rs +++ b/charon/src/bin/charon-driver/main.rs @@ -241,7 +241,6 @@ fn main() { trace!("Compiler arguments: {:?}", compiler_args); // Call the Rust compiler with our custom callback. - let errors_as_warnings = options.errors_as_warnings; let mut callback = CharonCallbacks::new(options); let mut res = callback.run_compiler(compiler_args); let CharonCallbacks { @@ -253,7 +252,7 @@ fn main() { if !options.no_serialize { // # Final step: generate the files. - if res.is_ok() || options.errors_as_warnings { + if res.is_ok() || !options.error_on_warnings { // `crate_data` is set by our callbacks when there is no fatal error. if let Some(crate_data) = crate_data { let dest_file = match options.dest_file.clone() { @@ -276,7 +275,7 @@ fn main() { } } - if !errors_as_warnings && matches!(res, Err(CharonFailure::Panic)) { + if options.error_on_warnings && matches!(res, Err(CharonFailure::Panic)) { // If we emitted any error, the call into rustc will panic. Hence we assume this is // just a normal failure. // TODO: emit errors ourselves to avoid this (#409). @@ -286,7 +285,7 @@ fn main() { match res { Ok(()) => { if error_count > 0 { - assert!(errors_as_warnings); + assert!(!options.error_on_warnings); let msg = format!("The extraction generated {} warnings", error_count); log::warn!("{}", msg); } @@ -296,7 +295,7 @@ fn main() { if matches!(err, CharonFailure::Panic) { // This is a real panic, exit with the standard rust panic error code. std::process::exit(101); - } else if !errors_as_warnings { + } else if options.error_on_warnings { std::process::exit(1); } } diff --git a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs index e7da2e806..7a0027864 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs @@ -368,7 +368,6 @@ pub fn translate<'tcx, 'ctx>(options: &CliOpts, tcx: TyCtxt<'tcx>) -> TransformC tcx, hax::options::Options { inline_macro_calls: Vec::new(), - // downgrade_errors: options.errors_as_warnings, }, ); @@ -386,7 +385,7 @@ pub fn translate<'tcx, 'ctx>(options: &CliOpts, tcx: TyCtxt<'tcx>) -> TransformC let mut error_ctx = ErrorCtx { continue_on_failure: !options.abort_on_error, - errors_as_warnings: options.errors_as_warnings, + error_on_warnings: options.error_on_warnings, dcx: tcx.dcx(), external_decls_with_errors: HashSet::new(), ignored_failed_decls: HashSet::new(), diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index 31a3e44bc..191018b87 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -949,7 +949,6 @@ fn main() -> Result<()> { // Call charon on itself let mut cmd = Command::cargo_bin("charon")?; cmd.arg("--cargo-arg=--lib"); - cmd.arg("--errors-as-warnings"); cmd.arg("--hide-marker-traits"); cmd.arg("--dest-file"); cmd.arg(&charon_llbc); diff --git a/charon/src/errors.rs b/charon/src/errors.rs index 826577aa4..b6a7dc9b0 100644 --- a/charon/src/errors.rs +++ b/charon/src/errors.rs @@ -68,8 +68,8 @@ pub struct DepSource { pub struct ErrorCtx<'ctx> { /// If true, do not abort on the first error and attempt to extract as much as possible. pub continue_on_failure: bool, - /// If true, print the errors as warnings, and do not abort. - pub errors_as_warnings: bool, + /// If true, print the warnings as errors, and abort if any errors were raised. + pub error_on_warnings: bool, /// The compiler session, used for displaying errors. #[cfg(feature = "rustc")] @@ -106,19 +106,19 @@ impl ErrorCtx<'_> { msg: &str, ) { let msg = msg.to_string(); - if self.errors_as_warnings { - self.dcx.span_warn(span, msg); - } else { + if self.error_on_warnings { self.dcx.span_err(span, msg); + } else { + self.dcx.span_warn(span, msg); } } #[cfg(not(feature = "rustc"))] pub(crate) fn span_err_no_register(&self, _span: Span, msg: &str) { let msg = msg.to_string(); if self.errors_as_warnings { - error!("{}", msg); - } else { warn!("{}", msg); + } else { + error!("{}", msg); } } diff --git a/charon/src/options.rs b/charon/src/options.rs index 596115d06..24b53f88a 100644 --- a/charon/src/options.rs +++ b/charon/src/options.rs @@ -177,9 +177,9 @@ pub struct CliOpts { #[serde(default)] pub abort_on_error: bool, /// Print the errors as warnings - #[clap(long = "errors-as-warnings", help = "Report the errors as warnings")] + #[clap(long = "error-on-warnings", help = "Consider any warnings as errors")] #[serde(default)] - pub errors_as_warnings: bool, + pub error_on_warnings: bool, #[clap( long = "no-serialize", help = "Don't serialize the final (U)LLBC to a file." @@ -231,10 +231,5 @@ impl CliOpts { !self.mir_promoted || !self.mir_optimized, "Can't use --mir_promoted and --mir_optimized at the same time" ); - - assert!( - !self.abort_on_error || !self.errors_as_warnings, - "Can't use --abort-on-error and --errors-as-warnings at the same time" - ); } } diff --git a/charon/tests/cargo.rs b/charon/tests/cargo.rs index de1867d34..9693c91e5 100644 --- a/charon/tests/cargo.rs +++ b/charon/tests/cargo.rs @@ -29,6 +29,7 @@ fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> { // Call charon let mut cmd = Command::cargo_bin("charon")?; cmd.current_dir(&test_case.dir); + cmd.arg("--error-on-warnings"); cmd.arg("--print-llbc"); cmd.arg("--dest-file"); cmd.arg(test_case.expected.with_extension("llbc")); diff --git a/charon/tests/popular-crates.rs b/charon/tests/popular-crates.rs index b28f13b2e..3d1732a74 100644 --- a/charon/tests/popular-crates.rs +++ b/charon/tests/popular-crates.rs @@ -102,7 +102,6 @@ fn process_crate(version: &Version) -> Result<()> { .stderr(Stdio::piped()) .current_dir(&crate_dir) .arg("--hide-marker-traits") - .arg("--errors-as-warnings") .arg("--dest-file") .arg(&llbc_path) .spawn()?; diff --git a/charon/tests/ui.rs b/charon/tests/ui.rs index cc780eb22..4da5c1e4e 100644 --- a/charon/tests/ui.rs +++ b/charon/tests/ui.rs @@ -177,6 +177,7 @@ fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> { let mut cmd = Command::cargo_bin("charon")?; cmd.arg("--no-cargo"); + cmd.arg("--error-on-warnings"); cmd.arg("--print-llbc"); cmd.arg("--crate=test_crate"); cmd.arg("--input"); diff --git a/charon/tests/ui/trait-instance-id.rs b/charon/tests/ui/trait-instance-id.rs index 25693b71e..e8b1c92d9 100644 --- a/charon/tests/ui/trait-instance-id.rs +++ b/charon/tests/ui/trait-instance-id.rs @@ -1,4 +1,3 @@ -//@ charon-args=--errors-as-warnings // This (for now) produces `TraitRefKind::Unknown`; it's a regression test because we used to // not parse this in `charon-ml`. fn main() {