Ugly commit.

prusti-viper/src/encoder/high/procedures/inference/visitor/mod.rs

@@ -223,7 +223,7 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
         self.process_actions(actions)?;
         state.remove_permissions(&consumed_permissions)?;
         state.insert_permissions(produced_permissions)?;
-        match &statement {
+        match statement {
             vir_typed::Statement::ObtainMutRef(_) => {
                 // The requirements already performed the needed changes.
             }
@@ -261,7 +261,7 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
                     .push(statement.typed_to_middle_statement(self.encoder)?);
             }
             vir_typed::Statement::Pack(pack_statement) => {
-                state.remove_manually_managed(&pack_statement.place)?;
+                // state.remove_manually_managed(&pack_statement.place)?;
                 let position = pack_statement.position();
                 let place = pack_statement
                     .place
@@ -271,7 +271,7 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
                 self.current_statements.push(encoded_statement);
             }
             vir_typed::Statement::Unpack(unpack_statement) => {
-                state.insert_manually_managed(unpack_statement.place.clone())?;
+                // state.insert_manually_managed(unpack_statement.place.clone())?;
                 let position = unpack_statement.position();
                 let place = unpack_statement
                     .place
@@ -297,7 +297,7 @@ impl<'p, 'v, 'tcx> Visitor<'p, 'v, 'tcx> {
                 self.current_statements.push(encoded_statement);
             }
             vir_typed::Statement::ForgetInitialization(forget_statement) => {
-                state.insert_manually_managed(forget_statement.place.clone())?;
+                // state.insert_manually_managed(forget_statement.place.clone())?;
                 let position = forget_statement.position();
                 let place = forget_statement
                     .place

prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs

@@ -2315,33 +2315,39 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinMethodsInterface for Lowerer<'p, 'v, 'tcx> {
                 source_snapshot.clone(),
                 source_permission_amount,
             )?];
-            let new_snapshot = self.new_snapshot_variable_version(&target.get_base(), position)?;
-            self.encode_snapshot_update_with_new_snapshot(
+            let new_snapshot = self.encode_snapshot_update_with_new_snapshot(
                 &mut copy_place_statements,
                 &target,
                 source_snapshot,
                 position,
-                Some(new_snapshot.clone()),
+                // Some(new_snapshot.clone()),
             )?;
             if let Some(conditions) = value.use_field {
                 let mut disjuncts = Vec::new();
                 for condition in conditions {
                     disjuncts.push(self.lower_block_marker_condition(condition)?);
                 }
                 let mut else_branch = vec![assign_statement];
-                self.encode_snapshot_update_with_new_snapshot(
+                let new_snapshot_else_branch = self.encode_snapshot_update_with_new_snapshot(
                     &mut else_branch,
                     &target,
                     result_value.into(),
                     position,
-                    Some(new_snapshot),
+                    // Some(new_snapshot),
                 )?;
                 statements.push(vir_low::Statement::conditional(
                     disjuncts.into_iter().disjoin(),
                     copy_place_statements,
                     else_branch,
                     position,
                 ));
+                statements.push(vir_low::Statement::assume(
+                    vir_low::Expression::equals(
+                        new_snapshot,
+                        new_snapshot_else_branch,
+                    ),
+                    position,
+                ));
             } else {
                 // Use field unconditionally.
                 statements.extend(copy_place_statements);

prusti-viper/src/encoder/middle/core_proof/into_low/cfg.rs

@@ -639,7 +639,6 @@ impl IntoLow for vir_mid::Statement {
                     &mut statements,
                     union_place,
                     statement.position,
-                    None,
                 )?;
                 let snapshot = union_place.to_procedure_snapshot(lowerer)?;
                 let discriminant = lowerer.obtain_enum_discriminant(

prusti-viper/src/encoder/middle/core_proof/snapshots/variables/interface.rs

@@ -38,6 +38,8 @@ trait Private {
         version: u64,
     ) -> SpannedEncodingResult<vir_low::VariableDecl>;
     #[allow(clippy::ptr_arg)] // Clippy false positive.
+    /// Note: if `new_snapshot_root` is `Some`, the current encoding assumes
+    /// that the `place` is not behind a raw pointer.
     fn snapshot_copy_except(
         &mut self,
         statements: &mut Vec<vir_low::Statement>,
@@ -380,16 +382,16 @@ pub(in super::super::super) trait SnapshotVariablesInterface {
         statements: &mut Vec<vir_low::Statement>,
         target: &vir_mid::Expression,
         position: vir_low::Position,
-        new_snapshot: Option<vir_low::VariableDecl>,
+        // new_snapshot: Option<vir_low::VariableDecl>,
     ) -> SpannedEncodingResult<vir_low::Expression>;
     fn encode_snapshot_update_with_new_snapshot(
         &mut self,
         statements: &mut Vec<vir_low::Statement>,
         target: &vir_mid::Expression,
         value: vir_low::Expression,
         position: vir_low::Position,
-        new_snapshot: Option<vir_low::VariableDecl>,
-    ) -> SpannedEncodingResult<()>;
+        // new_snapshot: Option<vir_low::VariableDecl>,
+    ) -> SpannedEncodingResult<vir_low::Expression>;
     #[allow(clippy::ptr_arg)] // Clippy false positive.
     fn encode_snapshot_update(
         &mut self,
@@ -562,7 +564,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> SnapshotVariablesInterface for Lowerer<'p, 'v, 'tcx>
         statements: &mut Vec<vir_low::Statement>,
         target: &vir_mid::Expression,
         position: vir_low::Position,
-        new_snapshot: Option<vir_low::VariableDecl>,
+        // new_snapshot_root: Option<vir_low::VariableDecl>,
     ) -> SpannedEncodingResult<vir_low::Expression> {
         // let base = target.get_base();
         // self.ensure_type_definition(&base.ty)?;
@@ -614,21 +616,23 @@ impl<'p, 'v: 'p, 'tcx: 'v> SnapshotVariablesInterface for Lowerer<'p, 'v, 'tcx>
         Ok(new_snapshot)
         // }
     }
+    /// `new_snapshot_root` is used when we want to use a specific variable
+    /// version as the root of the new snapshot.
     fn encode_snapshot_update_with_new_snapshot(
         &mut self,
         statements: &mut Vec<vir_low::Statement>,
         target: &vir_mid::Expression,
         value: vir_low::Expression,
         position: vir_low::Position,
-        new_snapshot: Option<vir_low::VariableDecl>,
-    ) -> SpannedEncodingResult<()> {
+        // new_snapshot_root: Option<vir_low::VariableDecl>,
+    ) -> SpannedEncodingResult<vir_low::Expression> {
         use vir_low::macros::*;
         // self.encode_snapshot_havoc(statements, target, position, new_snapshot)?;
         // statements
         //     .push(stmtp! { position => assume ([target.to_procedure_snapshot(self)?] == [value]) });
         let new_snapshot = self.encode_snapshot_havoc(statements, target, position)?;
-        statements.push(stmtp! { position => assume ([new_snapshot] == [value]) });
-        Ok(())
+        statements.push(stmtp! { position => assume ([new_snapshot.clone()] == [value]) });
+        Ok(new_snapshot)
     }
     fn encode_snapshot_update(
         &mut self,
@@ -637,7 +641,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> SnapshotVariablesInterface for Lowerer<'p, 'v, 'tcx>
         value: vir_low::Expression,
         position: vir_low::Position,
     ) -> SpannedEncodingResult<()> {
-        self.encode_snapshot_update_with_new_snapshot(statements, target, value, position, None)
+        self.encode_snapshot_update_with_new_snapshot(statements, target, value, position)?;
+        Ok(())
     }
     /// `basic_block_edges` are statements to be executed then going from one
     /// block to another.

prusti-viper/src/encoder/mir/types/encoder.rs

@@ -200,7 +200,7 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> {
                 //             .unwrap();
                 //         (array_len.into(), &[])
                 //     };
-                let array_len: usize = self.compute_array_len(*size).try_into().unwrap();
+                let array_len: usize = self.compute_array_len(*size).with_span(self.get_definition_span())?.try_into().unwrap();
                 let lifetimes = self.encoder.get_lifetimes_from_type_high(*elem_ty)?;
                 vir::Type::array(
                     vir::ty::ConstGenericArgument::new(Some(Box::new(array_len.into()))),

vir/defs/middle/ast/rvalue.rs

@@ -17,7 +17,7 @@ pub enum Rvalue {
     // ThreadLocalRef(ThreadLocalRef),
     AddressOf(AddressOf),
     Len(Len),
-    // Cast(Cast),
+    Cast(Cast),
     BinaryOp(BinaryOp),
     CheckedBinaryOp(CheckedBinaryOp),
     // NullaryOp(NullaryOp),
@@ -67,6 +67,13 @@ pub struct Len {
     pub place: Expression,
 }
 
+#[display(fmt = "cast({} -> {})", operand, ty)]
+pub struct Cast {
+    // TODO: kind: CastKind,
+    pub operand: Operand,
+    pub ty: Type,
+}
+
 #[display(fmt = "{}({}, {})", kind, left, right)]
 pub struct BinaryOp {
     pub kind: BinaryOpKind,