From a7fc890f2bf8fdc8184f57cde95dc23e47f166f5 Mon Sep 17 00:00:00 2001
From: seanrion <45787907+seanrion@users.noreply.github.com>
Date: Wed, 7 Aug 2024 18:26:09 +0800
Subject: [PATCH] add verify_errors_as_warnings

---
 prusti-interface/src/prusti_error.rs | 8 ++++++--
 prusti-utils/src/config.rs           | 7 +++++++
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/prusti-interface/src/prusti_error.rs b/prusti-interface/src/prusti_error.rs
index 89b8683a3d3..85942ce2532 100644
--- a/prusti-interface/src/prusti_error.rs
+++ b/prusti-interface/src/prusti_error.rs
@@ -70,10 +70,14 @@ impl PrustiError {
     /// Report a verification error of the verified Rust code
     pub fn verification<S: ToString>(message: S, span: MultiSpan) -> Self {
         check_message(message.to_string());
-        PrustiError::new(
+        let mut error = PrustiError::new(
             format!("[Prusti: verification error] {}", message.to_string()),
             span,
-        )
+        );
+        if config::verify_errors_as_warnings() {
+            error.set_warning();
+        }
+        error
     }
 
     pub fn disabled_verification<S: ToString>(message: S, span: MultiSpan) -> Self {
diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs
index 2e46d55519c..0a7579d0a9d 100644
--- a/prusti-utils/src/config.rs
+++ b/prusti-utils/src/config.rs
@@ -106,6 +106,7 @@ lazy_static::lazy_static! {
         settings.set_default("use_more_complete_exhale", true).unwrap();
         settings.set_default("skip_unsupported_features", false).unwrap();
         settings.set_default("internal_errors_as_warnings", false).unwrap();
+        settings.set_default("verify_errors_as_warnings", false).unwrap();
         settings.set_default("allow_unreachable_unsupported_code", false).unwrap();
         settings.set_default("no_verify", false).unwrap();
         settings.set_default("no_verify_deps", false).unwrap();
@@ -972,6 +973,12 @@ pub fn internal_errors_as_warnings() -> bool {
     read_setting("internal_errors_as_warnings")
 }
 
+/// When enabled, verify errors are reported as warnings instead of errors.
+/// Used for testing.
+pub fn verify_errors_as_warnings() -> bool {
+    read_setting("verify_errors_as_warnings")
+}
+
 /// When enabled, unsupported code is encoded as `assert false`. This way error
 /// messages are reported only for unsupported code that is actually reachable.
 pub fn allow_unreachable_unsupported_code() -> bool {