diff --git a/Cargo.lock b/Cargo.lock index 58edba19034..1d77374b4a3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2073,7 +2073,7 @@ dependencies = [ [[package]] name = "prusti-specs" -version = "0.1.1" +version = "0.1.2" dependencies = [ "itertools", "proc-macro2", diff --git a/analysis/Cargo.toml b/analysis/Cargo.toml index b1cfae4ffd4..34a16587629 100644 --- a/analysis/Cargo.toml +++ b/analysis/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "analysis" version = "0.1.0" -authors = ["Federico Poli "] +authors = ["Prusti Devs "] edition = "2021" [dependencies] diff --git a/jni-gen/Cargo.toml b/jni-gen/Cargo.toml index a07bc209984..2dd0efa0672 100644 --- a/jni-gen/Cargo.toml +++ b/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 "] +authors = ["Prusti Devs "] license = "MPL-2.0" readme = "README.md" edition = "2021" diff --git a/prusti-common/Cargo.toml b/prusti-common/Cargo.toml index e86a86b3d6b..d0f64f63040 100644 --- a/prusti-common/Cargo.toml +++ b/prusti-common/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "prusti-common" version = "0.1.0" -authors = ["Julian Dunskus "] +authors = ["Prusti Devs "] edition = "2021" [lib] diff --git a/prusti-contracts-build/Cargo.toml b/prusti-contracts-build/Cargo.toml index 38101e0dde6..5e678b02649 100644 --- a/prusti-contracts-build/Cargo.toml +++ b/prusti-contracts-build/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "prusti-contracts-build" version = "0.1.0" -authors = ["Vytautas Astrauskas "] +authors = ["Prusti Devs "] edition = "2021" [build-dependencies] diff --git a/prusti-contracts/prusti-contracts-proc-macros/Cargo.toml b/prusti-contracts/prusti-contracts-proc-macros/Cargo.toml index 75287c1dc83..fc5774d1c0e 100644 --- a/prusti-contracts/prusti-contracts-proc-macros/Cargo.toml +++ b/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 "] 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] diff --git a/prusti-contracts/prusti-contracts/Cargo.toml b/prusti-contracts/prusti-contracts/Cargo.toml index 0bc4c90f482..21177b1cfaf 100644 --- a/prusti-contracts/prusti-contracts/Cargo.toml +++ b/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 "] 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" diff --git a/prusti-contracts/prusti-specs/Cargo.toml b/prusti-contracts/prusti-specs/Cargo.toml index 80b5bb85dff..35308089b40 100644 --- a/prusti-contracts/prusti-specs/Cargo.toml +++ b/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 "] edition = "2021" license = "MPL-2.0" diff --git a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/impls.rs b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/impls.rs index 9c0af3dd78d..2b3037d2340 100644 --- a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/impls.rs +++ b/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 syn::Result 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", )); } diff --git a/prusti-contracts/prusti-specs/src/specifications/preparser.rs b/prusti-contracts/prusti-specs/src/specifications/preparser.rs index 3a6dd8383b9..df45fbad30a 100644 --- a/prusti-contracts/prusti-specs/src/specifications/preparser.rs +++ b/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 { - 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 { - 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::*; diff --git a/prusti-contracts/prusti-std/Cargo.toml b/prusti-contracts/prusti-std/Cargo.toml index 20ef17067a1..dcd32a40031 100644 --- a/prusti-contracts/prusti-std/Cargo.toml +++ b/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 "] 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] diff --git a/prusti-interface/Cargo.toml b/prusti-interface/Cargo.toml index beeedb21270..f3a78a551b2 100644 --- a/prusti-interface/Cargo.toml +++ b/prusti-interface/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "prusti-interface" version = "0.1.0" -authors = ["Federico Poli "] +authors = ["Prusti Devs "] description = "Interface between prusti and prusti-viper" license = "MPL-2.0" readme = "README.md" diff --git a/prusti-launch/Cargo.toml b/prusti-launch/Cargo.toml index 42a5540cb9c..10d24e83df3 100644 --- a/prusti-launch/Cargo.toml +++ b/prusti-launch/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "prusti-launch" version = "0.1.0" -authors = ["Julian Dunskus "] +authors = ["Prusti Devs "] edition = "2021" [[bin]] diff --git a/prusti-rustc-interface/Cargo.toml b/prusti-rustc-interface/Cargo.toml index d8b13b7ceb8..a379c1fdefd 100644 --- a/prusti-rustc-interface/Cargo.toml +++ b/prusti-rustc-interface/Cargo.toml @@ -1,6 +1,7 @@ [package] name = "prusti-rustc-interface" version = "0.1.0" +authors = ["Prusti Devs "] edition = "2021" [dependencies] diff --git a/prusti-server/Cargo.toml b/prusti-server/Cargo.toml index 486948d434b..416a1bfee84 100644 --- a/prusti-server/Cargo.toml +++ b/prusti-server/Cargo.toml @@ -1,10 +1,10 @@ [package] -authors = ["Julian Dunskus "] -description = "Server-side logic & handling for Prusti" name = "prusti-server" -license = "MPL-2.0" version = "0.1.0" +authors = ["Prusti Devs "] edition = "2021" +license = "MPL-2.0" +description = "Server-side logic & handling for Prusti" [lib] test = true # we have unit tests diff --git a/prusti-smt-solver/Cargo.toml b/prusti-smt-solver/Cargo.toml index fab61b5a258..b1ce69b796b 100644 --- a/prusti-smt-solver/Cargo.toml +++ b/prusti-smt-solver/Cargo.toml @@ -1,6 +1,7 @@ [package] name = "prusti-smt-solver" version = "0.1.0" +authors = ["Prusti Devs "] edition = "2021" [[bin]] diff --git a/prusti-tests/Cargo.toml b/prusti-tests/Cargo.toml index 37d9b7d88aa..02f225f5912 100644 --- a/prusti-tests/Cargo.toml +++ b/prusti-tests/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "prusti-tests" version = "0.2.0" -authors = ["Federico Poli "] +authors = ["Prusti Devs "] edition = "2021" [dev-dependencies] diff --git a/prusti-utils/Cargo.toml b/prusti-utils/Cargo.toml index 443b2dfedfe..cbb235b8c0f 100644 --- a/prusti-utils/Cargo.toml +++ b/prusti-utils/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "prusti-utils" version = "0.1.0" -authors = ["Julian Dunskus "] +authors = ["Prusti Devs "] edition = "2021" [lib] diff --git a/prusti-viper/Cargo.toml b/prusti-viper/Cargo.toml index 03475bcd161..cf61d95407d 100644 --- a/prusti-viper/Cargo.toml +++ b/prusti-viper/Cargo.toml @@ -1,11 +1,11 @@ [package] -authors = ["Federico Poli "] -description = "Translation of MIR into Viper" name = "prusti-viper" -readme = "README.md" -license = "MPL-2.0" version = "0.1.0" +authors = ["Prusti Devs "] edition = "2021" +description = "Translation of MIR into Viper" +readme = "README.md" +license = "MPL-2.0" [lib] doctest = false # we have no doc tests diff --git a/prusti/Cargo.toml b/prusti/Cargo.toml index b643f3be8a3..94c7dd145ba 100644 --- a/prusti/Cargo.toml +++ b/prusti/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "prusti" version = "0.2.1" -authors = ["Vytautas Astrauskas "] +authors = ["Prusti Devs "] edition = "2021" [[bin]] diff --git a/smt-log-analyzer/Cargo.toml b/smt-log-analyzer/Cargo.toml index 7aeda5aa822..dbb05ee8735 100644 --- a/smt-log-analyzer/Cargo.toml +++ b/smt-log-analyzer/Cargo.toml @@ -1,6 +1,7 @@ [package] name = "smt-log-analyzer" version = "0.1.0" +authors = ["Prusti Devs "] edition = "2021" [[bin]] diff --git a/test-crates/Cargo.toml b/test-crates/Cargo.toml index 073570db72d..30d3504504e 100644 --- a/test-crates/Cargo.toml +++ b/test-crates/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "test-crates" version = "0.1.0" -authors = ["Federico Poli "] +authors = ["Prusti Devs "] edition = "2021" [dependencies] diff --git a/viper-sys/Cargo.toml b/viper-sys/Cargo.toml index 288613314f4..57ed39ecd09 100644 --- a/viper-sys/Cargo.toml +++ b/viper-sys/Cargo.toml @@ -1,12 +1,12 @@ [package] name = "viper-sys" version = "0.1.0" +authors = ["Prusti Devs "] +edition = "2021" description = "Low-level interface to Viper" -authors = ["Federico Poli "] -license = "MPL-2.0" readme = "README.md" +license = "MPL-2.0" build = "build.rs" -edition = "2021" [build-dependencies] jni-gen = { path = "../jni-gen" } diff --git a/viper/Cargo.toml b/viper/Cargo.toml index a0a43d4f9be..dde30767b3a 100644 --- a/viper/Cargo.toml +++ b/viper/Cargo.toml @@ -1,11 +1,11 @@ [package] name = "viper" version = "0.1.0" +authors = ["Prusti Devs "] +edition = "2021" description = "High-level interface to Viper" -authors = ["Federico Poli "] -license = "MPL-2.0" readme = "README.md" -edition = "2021" +license = "MPL-2.0" [dependencies] log = { version = "0.4", features = ["release_max_level_info"] } diff --git a/vir-gen/Cargo.toml b/vir-gen/Cargo.toml index 028874a398b..5395a2f2d62 100644 --- a/vir-gen/Cargo.toml +++ b/vir-gen/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "vir-gen" version = "0.1.0" -authors = ["Vytautas Astrauskas "] +authors = ["Prusti Devs "] edition = "2021" license = "MIT OR Apache-2.0" description = "A VIR generator." diff --git a/vir/Cargo.toml b/vir/Cargo.toml index 7a6bd8b5b4c..d7c1adb5657 100644 --- a/vir/Cargo.toml +++ b/vir/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "vir" version = "0.1.0" -authors = ["Vytautas Astrauskas "] +authors = ["Prusti Devs "] edition = "2021" [dependencies]