From 32001c26d2965d88e96b754d2dbf9cb6cc6f1ef1 Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Thu, 4 Jul 2024 15:38:40 +0200
Subject: [PATCH] Add an option to downgrade errors to warnings

---
 cli/driver/src/exporter.rs           |  1 +
 cli/options/src/lib.rs               |  1 +
 frontend/exporter/options/src/lib.rs |  4 +++-
 frontend/exporter/src/utils.rs       | 23 ++++++++++++++++++++---
 4 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs
index 7a62fa8af..483fd3d45 100644
--- a/cli/driver/src/exporter.rs
+++ b/cli/driver/src/exporter.rs
@@ -285,6 +285,7 @@ impl From<ExtractionCallbacks> for hax_frontend_exporter_options::Options {
     fn from(opts: ExtractionCallbacks) -> hax_frontend_exporter_options::Options {
         hax_frontend_exporter_options::Options {
             inline_macro_calls: opts.inline_macro_calls,
+            downgrade_errors: false,
         }
     }
 }
diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs
index e99d5f7e3..9cae7d00b 100644
--- a/cli/options/src/lib.rs
+++ b/cli/options/src/lib.rs
@@ -462,6 +462,7 @@ impl From<Options> for hax_frontend_exporter_options::Options {
     fn from(opts: Options) -> hax_frontend_exporter_options::Options {
         hax_frontend_exporter_options::Options {
             inline_macro_calls: opts.inline_macro_calls,
+            downgrade_errors: false,
         }
     }
 }
diff --git a/frontend/exporter/options/src/lib.rs b/frontend/exporter/options/src/lib.rs
index a19c79f70..f4bbbcbf2 100644
--- a/frontend/exporter/options/src/lib.rs
+++ b/frontend/exporter/options/src/lib.rs
@@ -63,7 +63,9 @@ impl Namespace {
     }
 }
 
-#[derive(Debug, Clone)]
+#[derive(Default, Debug, Clone)]
 pub struct Options {
     pub inline_macro_calls: Vec<Namespace>,
+    /// Whether to emit errors or downgrade them as warnings.
+    pub downgrade_errors: bool,
 }
diff --git a/frontend/exporter/src/utils.rs b/frontend/exporter/src/utils.rs
index fc5691f44..db8898a74 100644
--- a/frontend/exporter/src/utils.rs
+++ b/frontend/exporter/src/utils.rs
@@ -59,10 +59,27 @@ macro_rules! report {
     };
 }
 
-macro_rules! error { ($($tt:tt)*) => {$crate::utils::report!(error, $($tt)*)} }
-#[allow(unused_macros)]
+macro_rules! fatal {
+    ($s:ident $($tt:tt)*) => {
+        if $s.base().options.downgrade_errors {
+            // Report the error but don't tell rustc.
+            $crate::utils::report!(warn, $s $($tt)*);
+            panic!("Fatal error");
+        } else {
+            $crate::utils::report!(fatal, $s $($tt)*);
+        }
+    }
+}
+macro_rules! error {
+    ($s:ident $($tt:tt)*) => {
+        if $s.base().options.downgrade_errors {
+            $crate::utils::report!(warn, $s $($tt)*);
+        } else {
+            $crate::utils::report!(error, $s $($tt)*);
+        }
+    }
+}
 macro_rules! warning { ($($tt:tt)*) => {$crate::utils::report!(warn, $($tt)*)} }
-macro_rules! fatal { ($($tt:tt)*) => {$crate::utils::report!(fatal, $($tt)*)} }
 
 pub(crate) use format_with_context;
 pub(crate) use internal_helpers::_span_verb_base;