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