Merge pull request #1280 from viperproject/improvements

Add macros for returning spanned encoding errors

prusti-viper/src/encoder/errors/encoding_error.rs

@@ -71,33 +71,3 @@ impl From<SpannedEncodingError> for EncodingError {
         EncodingError::Spanned(other)
     }
 }
-
-#[macro_export]
-macro_rules! error_internal {
-    ($message:expr) => {
-        return Err($crate::encoder::errors::EncodingError::internal($message))
-    };
-    ($($tokens:tt)+) => {
-        return Err($crate::encoder::errors::EncodingError::internal(format!($($tokens)+)))
-    };
-}
-
-#[macro_export]
-macro_rules! error_incorrect {
-    ($message:expr) => {
-        return Err($crate::encoder::errors::EncodingError::incorrect($message))
-    };
-    ($($tokens:tt)+) => {
-        return Err($crate::encoder::errors::EncodingError::incorrect(format!($($tokens)+)))
-    };
-}
-
-#[macro_export]
-macro_rules! error_unsupported {
-    ($message:expr) => {
-        return Err($crate::encoder::errors::EncodingError::unsupported($message))
-    };
-    ($($tokens:tt)+) => {
-        return Err($crate::encoder::errors::EncodingError::unsupported(format!($($tokens)+)))
-    };
-}

prusti-viper/src/encoder/errors/macros.rs

@@ -0,0 +1,53 @@
+// © 2022, ETH Zurich
+//
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+
+#[macro_export]
+macro_rules! error_internal {
+    ($span:expr => $message:expr) => {
+        return Err($crate::encoder::errors::SpannedEncodingError::internal($message), $span)
+    };
+    ($span:expr => $($tokens:tt)+) => {
+        return Err($crate::encoder::errors::SpannedEncodingError::internal(format!($($tokens)+), $span))
+    };
+    ($message:expr) => {
+        return Err($crate::encoder::errors::EncodingError::internal($message))
+    };
+    ($($tokens:tt)+) => {
+        return Err($crate::encoder::errors::EncodingError::internal(format!($($tokens)+)))
+    };
+}
+
+#[macro_export]
+macro_rules! error_incorrect {
+    ($span:expr => $message:expr) => {
+        return Err($crate::encoder::errors::SpannedEncodingError::incorrect($message), $span)
+    };
+    ($span:expr => $($tokens:tt)+) => {
+        return Err($crate::encoder::errors::SpannedEncodingError::incorrect(format!($($tokens)+), $span))
+    };
+    ($message:expr) => {
+        return Err($crate::encoder::errors::EncodingError::incorrect($message))
+    };
+    ($($tokens:tt)+) => {
+        return Err($crate::encoder::errors::EncodingError::incorrect(format!($($tokens)+)))
+    };
+}
+
+#[macro_export]
+macro_rules! error_unsupported {
+    ($span:expr => $message:expr) => {
+        return Err($crate::encoder::errors::SpannedEncodingError::unsupported($message), $span)
+    };
+    ($span:expr => $($tokens:tt)+) => {
+        return Err($crate::encoder::errors::SpannedEncodingError::unsupported(format!($($tokens)+), $span))
+    };
+    ($message:expr) => {
+        return Err($crate::encoder::errors::EncodingError::unsupported($message))
+    };
+    ($($tokens:tt)+) => {
+        return Err($crate::encoder::errors::EncodingError::unsupported(format!($($tokens)+)))
+    };
+}

prusti-viper/src/encoder/errors/mod.rs

@@ -11,6 +11,7 @@ pub use self::encoding_error::*;
 pub use self::encoding_error_kind::*;
 pub use self::with_span::*;
 pub use self::position_manager::*;
+pub use self::macros::*;
 pub use prusti_rustc_interface::errors::MultiSpan;
 
 mod conversions;
@@ -20,3 +21,4 @@ mod encoding_error;
 mod encoding_error_kind;
 mod with_span;
 mod position_manager;
+mod macros;