Merge remote-tracking branch 'upstream/master' into iterators-feature…

…-flag

prusti-interface/src/environment/mod.rs

@@ -16,6 +16,7 @@ use prusti_rustc_interface::middle::ty::TypeSuperFoldable;
 use std::path::PathBuf;
 use prusti_rustc_interface::errors::{DiagnosticBuilder, EmissionGuarantee, MultiSpan};
 use prusti_rustc_interface::span::{Span, symbol::Symbol};
+use prusti_common::config;
 use std::collections::HashSet;
 use log::{debug, trace};
 use std::rc::Rc;

prusti-specs/src/specifications/preparser.rs

@@ -893,7 +893,7 @@ mod tests {
             "forall (() , # [prusti :: spec_only] | x : i32 | -> bool { (((! (a) || (b))) : bool) })",
         );
         assert_eq!(
-            parse_prusti(quote! { exists(|x: i32| a === b) }).unwrap().to_string(),
+            parse_prusti("exists(|x: i32| a === b)".parse().unwrap()).unwrap().to_string(),
             "exists (() , # [prusti :: spec_only] | x : i32 | -> bool { ((snapshot_equality (& a , & b)) : bool) })",
         );
         assert_eq!(

prusti-viper/src/encoder/procedure_encoder.rs

@@ -2961,7 +2961,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         destination: mir::Place<'tcx>,
         target: Option<BasicBlockIndex>,
         called_def_id: ProcedureDefId,
-        mut substs: ty::subst::SubstsRef<'tcx>,
+        substs: ty::subst::SubstsRef<'tcx>,
     ) -> SpannedEncodingResult<Vec<vir::Stmt>> {
         let full_func_proc_name = &self
             .encoder
@@ -3000,6 +3000,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             })
             .collect();
 
+        // Spans for fake exprs that cannot be encoded in viper
+        let mut fake_expr_spans: FxHashMap<Local, Span> = FxHashMap::default();
+
         // Arguments can be places or constants. For constants, we pretend they're places by
         // creating a new local variable of the same type. For arguments that are not just local
         // variables (i.e., for places that have projections), we do the same. We don't replace