Ugly commit 2.

prusti-contracts/prusti-contracts/src/lib.rs

@@ -618,7 +618,8 @@ pub fn prusti_resolve<T>(_arg: T) {
 pub fn prusti_resolve_range<T>(
     _lifetime: &'static str,
     _arg: T,
-    _base_index: usize,
+    _predicate_range_start_index: usize,
+    _predicate_range_end_index: usize,
     _start_index: usize,
     _end_index: usize,
 ) {

prusti-contracts/prusti-specs/src/lib.rs

@@ -1505,15 +1505,23 @@ pub fn resolve(tokens: TokenStream) -> TokenStream {
 }
 
 pub fn resolve_range(tokens: TokenStream) -> TokenStream {
-    parse_expressions!(tokens, syn::Token![,] => lifetime_name, pointer, base_index, start_index, end_index);
+    parse_expressions!(tokens, syn::Token![,] =>
+        lifetime_name,
+        pointer,
+        predicate_range_start_index,
+        predicate_range_end_index,
+        start_index,
+        end_index
+    );
     // let (lifetime_name, pointer, base_index, start_index, end_index) =
     //     handle_result!(parse_five_expressions::<syn::Token![,]>(tokens));
     let lifetime_name_str = handle_result!(expression_to_string(&lifetime_name));
     unsafe_spec_function_call(quote! {
         prusti_resolve_range(
             #lifetime_name_str,
             std::ptr::addr_of!(#pointer),
-            {#base_index},
+            {#predicate_range_start_index},
+            {#predicate_range_end_index},
             {#start_index},
             {#end_index},
         )

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

@@ -1061,7 +1061,12 @@ impl IntoLow for vir_mid::Statement {
                 let start_address = statement.address.to_procedure_snapshot(lowerer)?;
                 // let start_address =
                 //     lowerer.pointer_address(ty, pointer_value, statement.position)?;
-                let base_index = statement.base_index.to_procedure_snapshot(lowerer)?;
+                let predicate_range_start_index = statement
+                    .predicate_range_start_index
+                    .to_procedure_snapshot(lowerer)?;
+                let predicate_range_end_index = statement
+                    .predicate_range_end_index
+                    .to_procedure_snapshot(lowerer)?;
                 let start_index = statement.start_index.to_procedure_snapshot(lowerer)?;
                 let end_index = statement.end_index.to_procedure_snapshot(lowerer)?;
                 let lifetime =
@@ -1106,8 +1111,8 @@ impl IntoLow for vir_mid::Statement {
                             ty,
                             target_type,
                             start_address.clone(),
-                            base_index.clone(),
-                            end_index.clone(),
+                            predicate_range_start_index.clone(),
+                            predicate_range_end_index.clone(),
                             lifetime.clone().into(),
                             true,
                             statement.position,

prusti-viper/src/encoder/mir/procedures/encoder/mod.rs

@@ -3900,15 +3900,18 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             Ok(true)
                         }
                         "prusti_contracts::prusti_resolve_range" => {
-                            assert_eq!(args.len(), 5);
+                            assert_eq!(args.len(), 6);
                             let mut encoded_args = extract_args(self.mir, args, block, self)?;
                             let ArgKind::Place(end_index) = encoded_args.pop().unwrap() else {
                                 unreachable!("Wrong function parameters?");
                             };
                             let ArgKind::Place(start_index) = encoded_args.pop().unwrap() else {
                                 unreachable!("Wrong function parameters?");
                             };
-                            let ArgKind::Place(base_index) = encoded_args.pop().unwrap() else {
+                            let ArgKind::Place(predicate_range_end_index) = encoded_args.pop().unwrap() else {
+                                unreachable!("Wrong function parameters?");
+                            };
+                            let ArgKind::Place(predicate_range_start_index) = encoded_args.pop().unwrap() else {
                                 unreachable!("Wrong function parameters?");
                             };
                             let ArgKind::Place(pointer) = encoded_args.pop().unwrap() else {
@@ -3931,7 +3934,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                                     lifetime,
                                     vir_high::ty::Uniqueness::Unique,
                                     pointer,
-                                    base_index,
+                                    predicate_range_start_index,
+                                    predicate_range_end_index,
                                     start_index,
                                     end_index,
                                 ),

vir/defs/high/ast/statement.rs

@@ -429,8 +429,11 @@ pub struct DeadReferenceRange {
     pub lifetime: LifetimeConst,
     pub uniqueness: Uniqueness,
     pub address: Expression,
-    /// We need this one to generate proper triggers.
-    pub base_index: Expression,
+    /// We need `predicate_range_start_index` and `predicate_range_end_index` to
+    /// be able to generate proper triggers: they are used to match the
+    /// `own_range!` predicate.
+    pub predicate_range_start_index: Expression,
+    pub predicate_range_end_index: Expression,
     pub start_index: Expression,
     pub end_index: Expression,
     pub position: Position,

vir/defs/middle/ast/statement.rs

@@ -454,8 +454,11 @@ pub struct DeadReferenceRange {
     pub lifetime: LifetimeConst,
     pub uniqueness: Uniqueness,
     pub address: Expression,
-    /// We need this one to generate proper triggers.
-    pub base_index: Expression,
+    /// We need `predicate_range_start_index` and `predicate_range_end_index` to
+    /// be able to generate proper triggers: they are used to match the
+    /// `own_range!` predicate.
+    pub predicate_range_start_index: Expression,
+    pub predicate_range_end_index: Expression,
     pub start_index: Expression,
     pub end_index: Expression,
     pub position: Position,