Ugly commit 3ei3.

viperproject · Mar 12, 2023 · ed2bad7 · ed2bad7
1 parent 22290ed
commit ed2bad7
Showing 1 changed file with 0 additions and 29 deletions.
diff --git a/prusti-viper/src/encoder/high/procedures/inference/eval_using.rs b/prusti-viper/src/encoder/high/procedures/inference/eval_using.rs
@@ -16,14 +16,11 @@ pub(super) fn wrap_in_eval_using(
     state: &mut super::state::FoldUnfoldState,
     mut expression: vir_typed::Expression,
 ) -> SpannedEncodingResult<vir_typed::Expression> {
-    eprintln!("expression: {expression}");
     let accessed_places = strip_dereferences(expression.collect_all_places());
     let mut framing_places = Vec::new();
     let mut context_kinds = Vec::new();
     for accessed_place in accessed_places {
-        eprintln!("accessed_place: {accessed_place}");
         if let Some(old_wrap) = check_old_wraps_and_return_first(&accessed_place, None) {
-            eprintln!("old_wrap: {old_wrap}");
             assert!(
                 matches!(
                     old_wrap,
@@ -40,14 +37,6 @@ pub(super) fn wrap_in_eval_using(
             }
             continue;
         }
-        // if let Some(old_wrap) = accessed_place.get_first_old_label() {
-        //     eprintln!("old_wrap: {old_wrap}");
-        //     if !framing_places.contains(old_wrap) {
-        //         framing_places.push(old_wrap.clone());
-        //         context_kinds.push(vir_typed::EvalInContextKind::Old);
-        //     }
-        //     continue;
-        // }
         let predicates_state =
             if let Some(predicate_state) = state.try_get_predicates_state(&accessed_place)? {
                 predicate_state
@@ -64,7 +53,6 @@ pub(super) fn wrap_in_eval_using(
                 if let Some(framing_place) =
                     state.find_prefix(PermissionKind::Owned, &accessed_place)
                 {
-                    eprintln!("framing_place: {framing_place}");
                     if !framing_places.contains(&framing_place) {
                         framing_places.push(framing_place);
                         context_kinds.push(vir_typed::EvalInContextKind::Predicate);
@@ -88,11 +76,8 @@ pub(super) fn wrap_in_eval_using(
                         .unwrap();
                     error_incorrect!(span => "cannot use specifications to trigger unblocking of a blocked place");
                 } else {
-                    eprintln!("----------");
-                    eprintln!("state: {state}");
                     let constituent_places = state.collect_owned_with_prefix(&accessed_place)?;
                     for framing_place in &constituent_places {
-                        eprintln!("framing_place: {framing_place}");
                         if !framing_places.contains(framing_place) {
                             framing_places.push(framing_place.clone());
                             context_kinds.push(vir_typed::EvalInContextKind::Predicate);
@@ -132,20 +117,6 @@ pub(super) fn wrap_in_eval_using(
         };
         expression = vir_typed::Expression::eval_in(context, kind, expression, position);
     }
-
-    // let mut places: Vec<_> = expression.collect_unique_places().iter().map(|place| {
-    //     // Drop below pointer dereference.
-    //     if let Some(pointer) = place.get_first_dereferenced_pointer() {
-    //         pointer.clone()
-    //     } else {
-    //         place
-    //     }
-    // }).collect();
-
-    // eprintln!("expression: {expression}");
-    // for p in &places {
-    //     eprintln!("  place: {p}");
-    // }
     Ok(expression)
 }