Set --errors-as-warnings by default

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);
             }
         }

charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs

@@ -296,7 +296,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
             if res.is_err() {
                 ctx.span_err(
                     span,
-                    &format!("Ignoring the following item due to an error: {rust_id:?}"),
+                    &format!("Ignoring the following item due to a previous error: {rust_id:?}"),
                 );
                 ctx.errors.ignore_failed_decl(trans_id);
             }
@@ -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(),

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);

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,16 +106,16 @@ 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 {
+        if self.error_on_warnings {
             error!("{}", msg);
         } else {
             warn!("{}", msg);

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"
-        );
     }
 }

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"));

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()?;

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");

charon/tests/ui/error-dependencies.out

@@ -1,7 +1,7 @@
 error: Trait aliases are not supported
  --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/ptr/metadata.rs:81:1
 
-error: Ignoring the following item due to an error: core::ptr::metadata::Thin
+error: Ignoring the following item due to a previous error: core::ptr::metadata::Thin
  --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/ptr/metadata.rs:81:1
 
 error: The external definition `core::ptr::metadata::Thin` triggered errors. It is (transitively) used at the following location(s):

charon/tests/ui/generic-associated-types.out

@@ -4,7 +4,7 @@ error: Generic associated types are not supported
 5 |     type Item<'a>
   |     ^^^^^^^^^^^^^
 
-error: Ignoring the following item due to an error: test_crate::LendingIterator
+error: Ignoring the following item due to a previous error: test_crate::LendingIterator
  --> tests/ui/generic-associated-types.rs:4:1
   |
 4 | trait LendingIterator {
@@ -16,7 +16,7 @@ error: Generic associated types are not supported
 46 |         type Type<'b>: for<'c> Foo<&'a &'b &'c ()>;
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-error: Ignoring the following item due to an error: test_crate::lifetimes::Bar
+error: Ignoring the following item due to a previous error: test_crate::lifetimes::Bar
   --> tests/ui/generic-associated-types.rs:45:5
    |
 45 |     trait Bar<'a> {
@@ -28,7 +28,7 @@ error: Generic associated types are not supported
 13 |     type Item<'b> = &'b T;
    |     ^^^^^^^^^^^^^
 
-error: Ignoring the following item due to an error: test_crate::{impl#0}
+error: Ignoring the following item due to a previous error: test_crate::{impl#0}
   --> tests/ui/generic-associated-types.rs:12:1
    |
 12 | impl<'a, T> LendingIterator for Option<&'a T> {

charon/tests/ui/issue-378-ctor-as-fn.out

@@ -1,7 +1,7 @@
 error: Casting constructors to function pointers is not supported
  --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:579:5
 
-error: Ignoring the following item due to an error: core::option::Option::Some::{constructor#0}
+error: Ignoring the following item due to a previous error: core::option::Option::Some::{constructor#0}
  --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:579:5
 
 error: The external definition `core::option::Option::Some` triggered errors. It is (transitively) used at the following location(s):

charon/tests/ui/non-lifetime-gats.out

@@ -4,7 +4,7 @@ error: Generic associated types are not supported
 5 |     type Pointer<T>: Deref<Target = T>;
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-error: Ignoring the following item due to an error: test_crate::PointerFamily
+error: Ignoring the following item due to a previous error: test_crate::PointerFamily
  --> tests/ui/non-lifetime-gats.rs:4:1
   |
 4 | trait PointerFamily {
@@ -16,7 +16,7 @@ error: Generic associated types are not supported
 34 |         type Type<U>: Link<T>;
    |         ^^^^^^^^^^^^^^^^^^^^^
 
-error: Ignoring the following item due to an error: test_crate::moar_variables::Trait
+error: Ignoring the following item due to a previous error: test_crate::moar_variables::Trait
   --> tests/ui/non-lifetime-gats.rs:33:5
    |
 33 |     trait Trait<T> {
@@ -28,7 +28,7 @@ error: Generic associated types are not supported
 13 |     type Pointer<T> = Box<T>;
    |     ^^^^^^^^^^^^^^^
 
-error: Ignoring the following item due to an error: test_crate::{impl#0}
+error: Ignoring the following item due to a previous error: test_crate::{impl#0}
   --> tests/ui/non-lifetime-gats.rs:12:1
    |
 12 | impl PointerFamily for BoxFamily {
@@ -40,7 +40,7 @@ error: Generic associated types are not supported
 39 |         type Type<U> = (T, U);
    |         ^^^^^^^^^^^^
 
-error: Ignoring the following item due to an error: test_crate::moar_variables::{impl#1}
+error: Ignoring the following item due to a previous error: test_crate::moar_variables::{impl#1}
   --> tests/ui/non-lifetime-gats.rs:38:5
    |
 38 |     impl<T> Trait<Option<T>> for Foo {

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() {

charon/tests/ui/unsupported/advanced-const-generics.out

@@ -26,7 +26,7 @@ error: Constant parameters of non-literal type are not supported
 14 | fn foo<const X: Foo>() -> Foo {
    |        ^^^^^^^^^^^^
 
-error: Ignoring the following item due to an error: test_crate::foo
+error: Ignoring the following item due to a previous error: test_crate::foo
   --> tests/ui/unsupported/advanced-const-generics.rs:14:1
    |
 14 | fn foo<const X: Foo>() -> Foo {

charon/tests/ui/unsupported/unbound-lifetime.out

@@ -18,7 +18,7 @@ error: Could not find region: Region { kind: ReError(ErrorGuaranteed { todo: "Er
 5 | fn get(_x: &'a u32) {}
   | ^^^^^^^^^^^^^^^^^^^^^^
 
-error: Ignoring the following item due to an error: test_crate::get
+error: Ignoring the following item due to a previous error: test_crate::get
  --> tests/ui/unsupported/unbound-lifetime.rs:5:1
   |
 5 | fn get(_x: &'a u32) {}

charon/tests/ui/unsupported/well-formedness-bound.out

@@ -4,7 +4,7 @@ error: Well-formedness clauses are unsupported
 4 |     &'a ():,
   |     ^^^^^^
 
-error: Ignoring the following item due to an error: test_crate::get
+error: Ignoring the following item due to a previous error: test_crate::get
  --> tests/ui/unsupported/well-formedness-bound.rs:2:1
   |
 2 | / fn get<'a>(x: &'a u32) -> Option<&'a u32>