Fix unwrap error when prusti-contracts compiled with stable

analysis/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "analysis"
 version = "0.1.0"
-authors = ["Federico Poli <federpoli@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [dependencies]

jni-gen/Cargo.toml

@@ -2,7 +2,7 @@
 name = "jni-gen"
 version = "0.1.0"
 description = "Generator of Rust bindings to Java classes"
-authors = ["Federico Poli <federpoli@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 license = "MPL-2.0"
 readme = "README.md"
 edition = "2021"

prusti-common/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "prusti-common"
 version = "0.1.0"
-authors = ["Julian Dunskus <julian.dunskus@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [lib]

prusti-contracts-build/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "prusti-contracts-build"
 version = "0.1.0"
-authors = ["Vytautas Astrauskas <vastrauskas@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [build-dependencies]

prusti-contracts/prusti-contracts-proc-macros/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-contracts-proc-macros"
-version = "0.1.1"
+version = "0.1.2"
 authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 license = "MPL-2.0"
@@ -15,7 +15,7 @@ categories = ["development-tools", "development-tools::testing"]
 proc-macro = true
 
 [dependencies]
-prusti-specs = { path = "../prusti-specs", version = "0.1.1", optional = true }
+prusti-specs = { path = "../prusti-specs", version = "0.1.2", optional = true }
 proc-macro2 = { version = "1.0", optional = true }
 
 [features]

prusti-contracts/prusti-contracts/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-contracts"
-version = "0.1.1"
+version = "0.1.2"
 authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 license = "MPL-2.0"
@@ -12,7 +12,7 @@ keywords = ["prusti", "contracts", "verification", "formal", "specifications"]
 categories = ["development-tools", "development-tools::testing"]
 
 [dependencies]
-prusti-contracts-proc-macros = { path = "../prusti-contracts-proc-macros", version = "0.1.1" }
+prusti-contracts-proc-macros = { path = "../prusti-contracts-proc-macros", version = "0.1.2" }
 
 [dev-dependencies]
 trybuild = "1.0"

prusti-contracts/prusti-specs/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-specs"
-version = "0.1.1"
+version = "0.1.2"
 authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 license = "MPL-2.0"

prusti-contracts/prusti-specs/src/extern_spec_rewriter/impls.rs

@@ -32,8 +32,7 @@ fn rewrite_extern_spec_internal(item_impl: &syn::ItemImpl) -> syn::Result<Rewrit
         #struct_ident #generic_args
     };
 
-    if item_impl.trait_.is_some() {
-        let (_, trait_path, _) = item_impl.trait_.as_ref().unwrap();
+    if let Some((_, trait_path, _)) = &item_impl.trait_ {
         if has_generic_arguments(trait_path) {
             return Err(syn::Error::new(
                 item_impl.generics.params.span(),

prusti-contracts/prusti-specs/src/extern_spec_rewriter/traits.rs

@@ -66,9 +66,8 @@ fn generate_new_struct(item_trait: &syn::ItemTrait) -> syn::Result<GeneratedStru
     };
 
     // Add a where clause which restricts this self type parameter to the trait
-    if item_trait.generics.where_clause.as_ref().is_some() {
-        let span = item_trait.generics.where_clause.as_ref().unwrap().span();
-        return Err(syn::Error::new(span, "Where clauses for extern traits specs are not supported"));
+    if let Some(where_clause) = &item_trait.generics.where_clause {
+        return Err(syn::Error::new(where_clause.span(), "Where clauses for extern traits specs are not supported"));
     }
     let self_where_clause: syn::WhereClause = parse_quote! {
         where #self_type_ident: #self_type_trait
@@ -140,9 +139,9 @@ impl<'a> GeneratedStruct<'a> {
                     ));
                 }
                 syn::TraitItem::Method(trait_method) => {
-                    if trait_method.default.is_some() {
+                    if let Some(default) = &trait_method.default {
                         return Err(syn::Error::new(
-                            trait_method.default.as_ref().unwrap().span(),
+                            default.span(),
                             "Default methods in external trait specs are invalid",
                         ));
                     }

prusti-contracts/prusti-specs/src/specifications/preparser.rs

@@ -172,12 +172,10 @@ impl PrustiTokenStream {
     {
         let result = f(&mut self)?;
         if !self.is_empty() {
-            let start = self.tokens.front().unwrap().span();
-            let end = self.tokens.back().unwrap().span();
-            let span = start.join(end);
-            // this is None if the spans are not combinable, which seems to happen when running the cfg(tests) via cargo
-            let error_span = span.unwrap_or(start);
-            return err(error_span, "unexpected extra tokens");
+            let start = self.tokens.front().expect("unreachable").span();
+            let end = self.tokens.back().expect("unreachable").span();
+            let span = join_spans(start, end);
+            return err(span, "unexpected extra tokens");
         }
         Ok(result)
     }
@@ -227,12 +225,10 @@ impl PrustiTokenStream {
         TokenStream
     )> {
         let mut pledge_ops = self.split(PrustiBinaryOp::Rust(RustOp::Arrow), false);
-        let (reference, body) = if pledge_ops.len() == 1 {
-            (None, pledge_ops.pop().unwrap())
-        } else if pledge_ops.len() == 2 {
-            (Some(pledge_ops[0].expr_bp(0)?), pledge_ops.pop().unwrap())
-        } else {
-            return err(Span::call_site(), "too many arrows in assert_on_expiry");
+        let (reference, body) = match (pledge_ops.pop(), pledge_ops.pop(), pledge_ops.pop()) {
+            (Some(body), None, _) => (None, body),
+            (Some(body), Some(mut reference), None) => (Some(reference.expr_bp(0)?), body),
+            _ => return err(Span::call_site(), "too many arrows in assert_on_expiry"),
         };
         let mut body_parts = body.split(PrustiBinaryOp::Rust(RustOp::Comma), false);
         if body_parts.len() == 2 {
@@ -507,7 +503,7 @@ impl Parse for GhostConstraint {
         Ok(GhostConstraint {
             trait_bounds: parse_trait_bounds(input)?,
             comma: input.parse().map_err(with_ghost_constraint_example)?,
-            specs: PrustiTokenStream::new(input.parse().unwrap())
+            specs: PrustiTokenStream::new(input.parse().expect("Failed to parse GhostConstraint"))
                 .parse_rest(|pts| pts.pop_group_of_nested_specs(input.span()))?,
         })
     }
@@ -745,7 +741,7 @@ impl PrustiToken {
         p1: &Punct,
         p2: &Punct,
     ) -> Option<Self> {
-        let span = p1.span().join(p2.span()).unwrap();
+        let span = join_spans(p1.span(), p2.span());
         Some(Self::BinOp(span, if operator2("&&", p1, p2) {
             PrustiBinaryOp::And
         } else if operator2("||", p1, p2) {
@@ -786,7 +782,7 @@ impl PrustiToken {
         p2: &Punct,
         p3: &Punct,
     ) -> Option<Self> {
-        let span = p1.span().join(p2.span()).unwrap().join(p3.span()).unwrap();
+        let span = join_spans(join_spans(p1.span(), p2.span()), p3.span());
         Some(Self::BinOp(span, if operator3("==>", p1, p2, p3) {
             PrustiBinaryOp::Implies
         } else if operator3("===", p1, p2, p3) {
@@ -908,6 +904,18 @@ impl RustOp {
     }
 }
 
+fn join_spans(s1: Span, s2: Span) -> Span {
+    // Tests don't run in the proc macro context
+    let is_proc_macro = std::panic::catch_unwind(|| s1.unwrap()).is_ok();
+    if is_proc_macro {
+        // This works even when compiled with stable
+        s1.unwrap().join(s2.unwrap()).expect("Failed to join spans!").into()
+    } else {
+        // During tests we don't care so much about returning a default
+        s1.join(s2).unwrap_or(s1)
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;

prusti-contracts/prusti-std/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "prusti-std"
-version = "0.1.1"
+version = "0.1.2"
 authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 license = "MPL-2.0"
@@ -12,7 +12,7 @@ keywords = ["prusti", "contracts", "verification", "formal", "specifications"]
 categories = ["development-tools", "development-tools::testing"]
 
 [dependencies]
-prusti-contracts = { path = "../prusti-contracts", version = "0.1.1" }
+prusti-contracts = { path = "../prusti-contracts", version = "0.1.2" }
 
 # Forward "prusti" flag
 [features]

prusti-interface/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "prusti-interface"
 version = "0.1.0"
-authors = ["Federico Poli <federpoli@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 description = "Interface between prusti and prusti-viper"
 license = "MPL-2.0"
 readme = "README.md"

prusti-launch/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "prusti-launch"
 version = "0.1.0"
-authors = ["Julian Dunskus <julian.dunskus@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [[bin]]

prusti-rustc-interface/Cargo.toml

@@ -1,6 +1,7 @@
 [package]
 name = "prusti-rustc-interface"
 version = "0.1.0"
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [dependencies]

prusti-server/Cargo.toml

@@ -1,10 +1,10 @@
 [package]
-authors = ["Julian Dunskus <julian.dunskus@gmail.com>"]
-description = "Server-side logic & handling for Prusti"
 name = "prusti-server"
-license = "MPL-2.0"
 version = "0.1.0"
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
+license = "MPL-2.0"
+description = "Server-side logic & handling for Prusti"
 
 [lib]
 test = true # we have unit tests

prusti-smt-solver/Cargo.toml

@@ -1,6 +1,7 @@
 [package]
 name = "prusti-smt-solver"
 version = "0.1.0"
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [[bin]]

prusti-tests/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "prusti-tests"
 version = "0.2.0"
-authors = ["Federico Poli <federpoli@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [dev-dependencies]

prusti-utils/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "prusti-utils"
 version = "0.1.0"
-authors = ["Julian Dunskus <julian.dunskus@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [lib]

prusti-viper/Cargo.toml

@@ -1,11 +1,11 @@
 [package]
-authors = ["Federico Poli <federpoli@gmail.com>"]
-description = "Translation of MIR into Viper"
 name = "prusti-viper"
-readme = "README.md"
-license = "MPL-2.0"
 version = "0.1.0"
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
+description = "Translation of MIR into Viper"
+readme = "README.md"
+license = "MPL-2.0"
 
 [lib]
 doctest = false # we have no doc tests

prusti/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "prusti"
 version = "0.2.1"
-authors = ["Vytautas Astrauskas <vastrauskas@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [[bin]]

smt-log-analyzer/Cargo.toml

@@ -1,6 +1,7 @@
 [package]
 name = "smt-log-analyzer"
 version = "0.1.0"
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [[bin]]

test-crates/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "test-crates"
 version = "0.1.0"
-authors = ["Federico Poli <federpoli@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [dependencies]

viper-sys/Cargo.toml

@@ -1,12 +1,12 @@
 [package]
 name = "viper-sys"
 version = "0.1.0"
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
+edition = "2021"
 description = "Low-level interface to Viper"
-authors = ["Federico Poli <federpoli@gmail.com>"]
-license = "MPL-2.0"
 readme = "README.md"
+license = "MPL-2.0"
 build = "build.rs"
-edition = "2021"
 
 [build-dependencies]
 jni-gen = { path = "../jni-gen" }

viper/Cargo.toml

@@ -1,11 +1,11 @@
 [package]
 name = "viper"
 version = "0.1.0"
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
+edition = "2021"
 description = "High-level interface to Viper"
-authors = ["Federico Poli <federpoli@gmail.com>"]
-license = "MPL-2.0"
 readme = "README.md"
-edition = "2021"
+license = "MPL-2.0"
 
 [dependencies]
 log = { version = "0.4", features = ["release_max_level_info"] }

vir-gen/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "vir-gen"
 version = "0.1.0"
-authors = ["Vytautas Astrauskas <vastrauskas@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 license = "MIT OR Apache-2.0"
 description = "A VIR generator."

vir/Cargo.toml

@@ -1,7 +1,7 @@
 [package]
 name = "vir"
 version = "0.1.0"
-authors = ["Vytautas Astrauskas <vastrauskas@gmail.com>"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 edition = "2021"
 
 [dependencies]