fix panic for unsupported for loops

reported as #387 (comment)

source/rust_verify/src/fn_call_to_vir.rs

@@ -90,6 +90,12 @@ pub(crate) fn fn_call_to_vir<'tcx>(
         Some(RustItem::TryTraitBranch) => {
             return err_span(expr.span, "Verus does not yet support the ? operator");
         }
+        Some(RustItem::IntoIterFn) => {
+            return err_span(
+                expr.span,
+                "Verus does not yet support IntoIterator::into_iter and for loops, use a while loop instead",
+            );
+        }
         _ => {}
     }
 

source/rust_verify/src/verus_items.rs

@@ -548,6 +548,7 @@ pub(crate) enum RustItem {
     IntIntrinsic(RustIntIntrinsicItem),
     AllocGlobal,
     TryTraitBranch,
+    IntoIterFn,
 }
 
 pub(crate) fn get_rust_item<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option<RustItem> {
@@ -582,6 +583,9 @@ pub(crate) fn get_rust_item<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option<Ru
     if tcx.lang_items().branch_fn() == Some(def_id) {
         return Some(RustItem::TryTraitBranch);
     }
+    if tcx.lang_items().into_iter_fn() == Some(def_id) {
+        return Some(RustItem::IntoIterFn);
+    }
 
     let rust_path = def_id_to_stable_rust_path(tcx, def_id);
     let rust_path = rust_path.as_ref().map(|x| x.as_str());

source/rust_verify_test/tests/regression.rs

@@ -558,3 +558,12 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_vir_error_msg(err, "unrecognized verifier attribute")
 }
+
+test_verify_one_file! {
+    #[test] test_for_loop_387_discussioncomment_5683342 verus_code! {
+        struct T{}
+        fn f(v: Vec<T>) {
+            for t in v {}
+        }
+    } => Err(err) => assert_vir_error_msg(err, "Verus does not yet support IntoIterator::into_iter")
+}