Merge #816

816: Update dependencies (nightly-2022-01-13) r=Aurel300 a=viper-admin * [x] Update rustc version to `nightly-2022-01-13`. * [x] Manualy update outdated dependencies (see the list below). * [x] Manualy run `cargo update`. <details><summary>List of direct outdated dependencies:</summary> ``` $ cargo outdated --root-deps-only --workspace info: syncing channel updates for 'nightly-2022-01-01-x86_64-unknown-linux-gnu' info: latest update on 2022-01-01, rust version 1.59.0-nightly (cfa3fe5af 2021-12-31) info: downloading component 'cargo' info: downloading component 'llvm-tools-preview' info: downloading component 'rust-std' info: downloading component 'rustc' info: downloading component 'rustc-dev' info: downloading component 'rustfmt' info: installing component 'cargo' info: installing component 'llvm-tools-preview' info: installing component 'rust-std' info: installing component 'rustc' info: installing component 'rustc-dev' info: installing component 'rustfmt' Updating git repository `https://github.com/rust-lang/cargo.git` analysis ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.131 --- 1.0.132 Normal --- syn 1.0.82 --- 1.0.84 Normal --- prusti-common ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.131 --- 1.0.132 Normal --- viper ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.131 --- 1.0.132 Normal --- viper-sys ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- ureq 2.3.1 --- 2.4.0 Build --- vir ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- proc-macro2 1.0.34 --- 1.0.36 Normal --- quote 1.0.10 --- 1.0.14 Normal --- serde 1.0.131 --- 1.0.132 Normal --- syn 1.0.82 --- 1.0.84 Normal --- vir-gen ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- proc-macro2 1.0.34 --- 1.0.36 Normal --- quote 1.0.10 --- 1.0.14 Normal --- syn 1.0.82 --- 1.0.84 Normal --- prusti-contracts-internal ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- proc-macro2 1.0.34 --- 1.0.36 Normal --- prusti-specs ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- proc-macro2 1.0.34 --- 1.0.36 Normal --- quote 1.0.10 --- 1.0.14 Normal --- serde 1.0.131 --- 1.0.132 Normal --- syn 1.0.82 --- 1.0.84 Normal --- prusti-interface ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.131 --- 1.0.132 Normal --- prusti-viper ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.131 --- 1.0.132 Normal --- prusti-server ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- clap 2.34.0 --- 3.0.0 Normal --- num_cpus 1.13.0 --- 1.13.1 Normal --- reqwest 0.10.10 --- 0.11.8 Normal --- serde 1.0.131 --- 1.0.132 Normal --- tokio 0.2.25 --- 1.15.0 Normal --- warp 0.2.5 --- 0.3.2 Normal --- prusti-launch ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- nix 0.23.0 --- 0.23.1 Normal cfg(unix) serde 1.0.131 --- 1.0.132 Normal --- test-crates ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.131 --- 1.0.132 Normal --- systest ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- ureq 2.3.1 --- 2.4.0 Build --- ``` </details> `@Aurel300` could you take care of this? Co-authored-by: Aurel Bílý <[email protected]> Co-authored-by: Vytautas Astrauskas <[email protected]>
viperproject · Jan 17, 2022 · bd02658 · bd02658
2 parents f7f3e1b + f8e1eaf
commit bd02658
Show file tree

Hide file tree

Showing 63 changed files with 420 additions and 367 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/analysis/src/domains/definitely_accessible/state.rs b/analysis/src/domains/definitely_accessible/state.rs
@@ -215,7 +215,7 @@ fn pretty_print_place<'tcx>(
                 variant = Some(variant_index);
             }
             mir::ProjectionElem::Field(field, field_ty) => {
-                let field_name = describe_field_from_ty(prev_ty, field, variant)?;
+                let field_name = describe_field_from_ty(tcx, prev_ty, field, variant)?;
                 pieces.push(format!(".{})", field_name));
                 prev_ty = field_ty;
                 variant = None;
@@ -234,13 +234,14 @@ fn pretty_print_place<'tcx>(
 
 /// End-user visible description of the `field_index`nth field of `ty`
 fn describe_field_from_ty(
+    tcx: TyCtxt<'_>,
     ty: ty::Ty<'_>,
     field: mir::Field,
     variant_index: Option<VariantIdx>,
 ) -> Option<String> {
     if ty.is_box() {
         // If the type is a box, the field is described from the boxed type
-        describe_field_from_ty(ty.boxed_ty(), field, variant_index)
+        describe_field_from_ty(tcx, ty.boxed_ty(), field, variant_index)
     } else {
         match *ty.kind() {
             ty::TyKind::Adt(def, _) => {
@@ -250,14 +251,14 @@ fn describe_field_from_ty(
                 } else {
                     def.non_enum_variant()
                 };
-                Some(variant.fields[field.index()].ident.to_string())
+                Some(variant.fields[field.index()].ident(tcx).to_string())
             }
             ty::TyKind::Tuple(_) => Some(field.index().to_string()),
             ty::TyKind::Ref(_, ty, _) | ty::TyKind::RawPtr(ty::TypeAndMut { ty, .. }) => {
-                describe_field_from_ty(ty, field, variant_index)
+                describe_field_from_ty(tcx, ty, field, variant_index)
             }
             ty::TyKind::Array(ty, _) | ty::TyKind::Slice(ty) => {
-                describe_field_from_ty(ty, field, variant_index)
+                describe_field_from_ty(tcx, ty, field, variant_index)
             }
             ty::TyKind::Closure(..) | ty::TyKind::Generator(..) => {
                 // Supporting these cases is complex

diff --git a/prusti-common/src/config/commandline.rs b/prusti-common/src/config/commandline.rs
@@ -6,22 +6,22 @@ use std::env;
 #[derive(Clone, Debug)]
 pub struct CommandLine {
     /// Optional prefix that will limit args to those that begin with the defined prefix.
-    /// 
+    ///
     /// Example: The arg -Zdebug=true would become debug=true with a prefix of -Z
     prefix: Option<String>,
 
-    /// Character sequence that separates key, value pairs. The default separator is '=', 
+    /// Character sequence that separates key, value pairs. The default separator is '=',
     /// the separator pattern must only occur once in the flag or it will be ignored.
-    /// 
+    ///
     /// Example: debug=true is a valid key,val pair with separator of '='
     ///          debug= would be invalid because there is no value.
-    ///          debug+true would be valid with a separator of '+' 
+    ///          debug+true would be valid with a separator of '+'
     separator: String,
 
     /// Boolean indicating whether invalid flags should be ignored or result in a ConfigError
-    /// 
+    ///
     /// Note: the method get_remaining_args always
-    ///       returns the invalid args regardless of this boolean 
+    ///       returns the invalid args regardless of this boolean
     ignore_invalid: bool,
 }
 
@@ -37,16 +37,19 @@ impl CommandLine {
         }
     }
 
+    #[must_use]
     pub fn prefix(mut self, s: &str) -> Self {
         self.prefix = Some(s.into());
         self
     }
 
+    #[must_use]
     pub fn separator(mut self, s: &str) -> Self {
         self.separator = s.into();
         self
     }
 
+    #[must_use]
     pub fn ignore_invalid(mut self, ignore: bool) -> Self {
         self.ignore_invalid = ignore;
         self
@@ -113,7 +116,7 @@ impl Source for CommandLine {
                 }
 
                 continue;
-            } 
+            }
 
             // If arg is valid this can't panic
             let (key, val) = self.split_arg(&arg[prefix_pattern.len()..])
@@ -123,7 +126,7 @@ impl Source for CommandLine {
                 key.to_lowercase(),
                 Value::new(Some(&uri), val),
             );
-        } 
+        }
 
         Ok(m)
     }

diff --git a/prusti-common/src/vir/optimizations/folding/expressions.rs b/prusti-common/src/vir/optimizations/folding/expressions.rs
@@ -27,6 +27,7 @@ use crate::vir::polymorphic_vir::FallibleExprFolder;
 
 
 pub trait FoldingOptimizer {
+    #[must_use]
     fn optimize(self) -> Self;
 }
 

diff --git a/prusti-common/src/vir/optimizations/functions/simplifier.rs b/prusti-common/src/vir/optimizations/functions/simplifier.rs
@@ -10,6 +10,7 @@ use crate::vir::polymorphic_vir::ast::{self, ExprFolder};
 
 pub trait Simplifier {
     /// Simplify by doing constant evaluation.
+    #[must_use]
     fn simplify(self) -> Self;
 }
 
@@ -26,6 +27,7 @@ impl Simplifier for ast::Function {
 }
 
 impl Simplifier for ast::Expr {
+    #[must_use]
     fn simplify(self) -> Self {
         let mut folder = ExprSimplifier {};
         folder.fold(self)

diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs
@@ -278,9 +278,9 @@ impl<'tcx> Environment<'tcx> {
     /// Get all relevant trait declarations for some type.
     pub fn get_traits_decls_for_type(&self, ty: &ty::Ty<'tcx>) -> HashSet<DefId> {
         let mut res = HashSet::new();
-        let traits = self.tcx().all_traits(());
-        for trait_id in traits.iter() {
-            self.tcx().for_each_relevant_impl(*trait_id, ty, |impl_id| {
+        let traits = self.tcx().all_traits();
+        for trait_id in traits {
+            self.tcx().for_each_relevant_impl(trait_id, ty, |impl_id| {
                 if let Some(relevant_trait_id) = self.tcx().trait_id_of_impl(impl_id) {
                     res.insert(relevant_trait_id);
                 }

diff --git a/prusti-interface/src/prusti_error.rs b/prusti-interface/src/prusti_error.rs
@@ -125,11 +125,13 @@ impl PrustiError {
         self.is_disabled
     }
 
+    #[must_use]
     pub fn set_help<S: ToString>(mut self, message: S) -> Self {
         self.help = Some(message.to_string());
         self
     }
 
+    #[must_use]
     pub fn add_note<S: ToString>(mut self, message: S, opt_span: Option<Span>) -> Self {
         self.notes.push((message.to_string(), opt_span.map(MultiSpan::from)));
         self
@@ -163,6 +165,7 @@ impl PrustiError {
     /// Set the span of the failing assertion expression.
     ///
     /// Note: this is a noop if `opt_span` is None
+    #[must_use]
     pub fn set_failing_assertion(mut self, opt_span: Option<&MultiSpan>) -> Self {
         if let Some(span) = opt_span {
             let note = "the failing assertion is here".to_string();
@@ -174,6 +177,7 @@ impl PrustiError {
     /// Convert the original error span to a note, and add a new error span.
     ///
     /// Note: this is a noop if `opt_span` is None
+    #[must_use]
     pub fn push_primary_span(mut self, opt_span: Option<&MultiSpan>) -> Self {
         if let Some(span) = opt_span {
             self.notes.push(("the error originates here".to_string(), Some(self.span)));

diff --git a/prusti-specs/src/specifications/common.rs b/prusti-specs/src/specifications/common.rs
@@ -367,6 +367,7 @@ impl<EID: Clone + Debug, ET: Clone + Debug, AT: Clone + Debug> ProcedureSpecific
     ///
     /// In other words, any pre-/post-condition provided by `other` will overwrite any provided by
     /// `self`.
+    #[must_use]
     pub fn refine(&self, other: &Self) -> Self {
         let pres = if other.pres.is_empty() {
             self.pres.clone()

diff --git a/prusti-specs/src/specifications/preparser.rs b/prusti-specs/src/specifications/preparser.rs
@@ -81,6 +81,7 @@ impl Parser {
         }
     }
     /// initializes the parser with a TokenStream and the last span
+    #[allow(clippy::wrong_self_convention)]
     fn from_token_stream_last_span(&self, tokens: TokenStream) -> Self {
         Self {
             tokens: tokens.into_iter().collect(),
@@ -373,6 +374,7 @@ impl Parser {
     }
 
     /// is there any non-prusti operator following the first thing?
+    #[allow(clippy::wrong_self_convention)]
     fn is_part_of_rust_expr(&mut self) -> bool {
         if let Some(token) = self.tokens.pop_front() {
             let result = !(self.peek_operator("|=") ||

diff --git a/prusti-specs/src/specifications/untyped.rs b/prusti-specs/src/specifications/untyped.rs
@@ -235,17 +235,17 @@ impl AssignExpressionId<TriggerSet> for common::TriggerSet<(), syn::Expr> {
         spec_id: SpecificationId,
         id_generator: &mut ExpressionIdGenerator,
     ) -> TriggerSet {
-        TriggerSet {
-            0: self.0
+        common::TriggerSet(
+            self.0
                 .into_iter()
-                .map(|x| common::Trigger {
-                    0: x.0
+                .map(|x| common::Trigger(
+                    x.0
                         .into_iter()
                         .map(|y| y.assign_id(spec_id, id_generator))
                         .collect()
-                })
+                ))
                 .collect()
-        }
+        )
     }
 }
 

diff --git a/prusti-tests/tests/cargo_verify/prusti_toml/output.stdout b/prusti-tests/tests/cargo_verify/prusti_toml/output.stdout
@@ -20,7 +20,7 @@ fn prusti_post_item_test1_[..](result: ()) {
     || -> bool { false };
 }
 #[prusti::post_spec_id_ref = "[..]"]
-pub fn test1() { }
+pub fn test1() {}
 pub fn test2() {
     if !false { ::core::panicking::panic("assertion failed: false") };
 }

diff --git a/prusti-tests/tests/parse/ui/after_expiry.stdout b/prusti-tests/tests/parse/ui/after_expiry.stdout
@@ -42,7 +42,7 @@ fn prusti_post_item_test1_$(NUM_UUID)(a: bool,
 }
 #[prusti::pledge_spec_id_ref =
   "$(NUM_UUID):$(NUM_UUID)"]
-fn test1(a: bool) { }
+fn test1(a: bool) {}
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
@@ -69,7 +69,7 @@ fn prusti_post_item_test2_$(NUM_UUID)(a: bool,
 }
 #[prusti::pledge_spec_id_ref =
   "$(NUM_UUID):$(NUM_UUID)"]
-fn test2(a: bool) { }
+fn test2(a: bool) {}
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
@@ -83,7 +83,7 @@ fn prusti_post_item_test3_$(NUM_UUID)(a: bool,
     || -> bool { a };
 }
 #[prusti::pledge_spec_id_ref = ":$(NUM_UUID)"]
-fn test3(a: bool) { }
+fn test3(a: bool) {}
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
@@ -97,7 +97,7 @@ fn prusti_post_item_test4_$(NUM_UUID)(a: bool,
     || -> bool { a };
 }
 #[prusti::pledge_spec_id_ref = ":$(NUM_UUID)"]
-fn test4(a: bool) { }
+fn test4(a: bool) {}
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]

diff --git a/prusti-tests/tests/parse/ui/and.stdout b/prusti-tests/tests/parse/ui/and.stdout
@@ -32,7 +32,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() {
     || -> bool { true };
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
-fn test1() { }
+fn test1() {}
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
@@ -53,7 +53,7 @@ fn prusti_pre_item_test2_$(NUM_UUID)() {
     || -> bool { true };
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
-fn test2() { }
+fn test2() {}
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
@@ -74,7 +74,7 @@ fn prusti_pre_item_test3_$(NUM_UUID)() {
     || -> bool { true };
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
-fn test3() { }
+fn test3() {}
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
@@ -95,7 +95,7 @@ fn prusti_pre_item_test4_$(NUM_UUID)() {
     || -> bool { true };
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
-fn test4() { }
+fn test4() {}
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
@@ -120,7 +120,7 @@ fn prusti_pre_item_test5_$(NUM_UUID)() {
     || -> bool { true };
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
-fn test5() { }
+fn test5() {}
 fn main() {}
 Procedure(ProcedureSpecification { pres: [Assertion { kind: And([Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:6 ~ and[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:7 ~ and[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#1}) }) }]) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false })
 Procedure(ProcedureSpecification { pres: [Assertion { kind: And([Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:10 ~ and[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#0}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:11 ~ and[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#1}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(103), expr: DefId(0:12 ~ and[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#2}) }) }]) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false })
-Original file line number
+Diff line change
@@ Expand Up / @@ -27,6 +27,7 @@ use crate::vir::polymorphic_vir::FallibleExprFolder; @@
     pub trait FoldingOptimizer {
+        #[must_use]
         fn optimize(self) -> Self;
     }
@@ Expand Down @@