bugfix: show 'not supported' error for let-else

partially addresses #1393
verus-lang · Jan 22, 2025 · f172d14 · f172d14
1 parent 1dcd13d
commit f172d14
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 4 deletions.
diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs
@@ -786,7 +786,11 @@ pub(crate) fn invariant_block_open<'a>(
                         ),
                     ..
                 }),
-            ..
+            els: None,
+            ty: _,
+            hir_id: _,
+            span: _,
+            source: _,
         }) if dot_dot_pos.as_opt_usize().is_none() => {
             let verus_item = verus_items.id_to_name.get(fun_id);
             let atomicity = match verus_item {
@@ -2007,7 +2011,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
         ExprKind::If(cond, lhs, rhs) => {
             let cond = cond.peel_drop_temps();
             match cond.kind {
-                ExprKind::Let(LetExpr { pat, init: expr, ty: _, span: _, .. }) => {
+                ExprKind::Let(LetExpr { pat, init: expr, ty: _, span: _, recovered: _ }) => {
                     // if let
                     let vir_expr = expr_to_vir(bctx, expr, modifier)?;
                     let mut vir_arms: Vec<vir::ast::Arm> = Vec::new();
@@ -2524,7 +2528,10 @@ fn unwrap_parameter_to_vir<'tcx>(
             },
         ty: None,
         init: None,
-        ..
+        els: None,
+        hir_id: _,
+        span: _,
+        source: _,
     }) = &stmt1.kind
     {
         Some((pat.hir_id, local_to_var(x, hir_id.local_id)))
@@ -2640,9 +2647,12 @@ pub(crate) fn stmt_to_vir<'tcx>(
                 unsupported_err!(stmt.span, "internal item statements", stmt)
             }
         }
-        StmtKind::Let(LetStmt { pat, ty: _, init, els: _, hir_id: _, span: _, source: _ }) => {
+        StmtKind::Let(LetStmt { pat, ty: _, init, els: None, hir_id: _, span: _, source: _ }) => {
             let_stmt_to_vir(bctx, pat, init, bctx.ctxt.tcx.hir().attrs(stmt.hir_id))
         }
+        StmtKind::Let(LetStmt { els: Some(_), .. }) => {
+            unsupported_err!(stmt.span, "let-else", stmt)
+        }
     }
 }
 

diff --git a/source/rust_verify_test/tests/match.rs b/source/rust_verify_test/tests/match.rs
@@ -1218,3 +1218,14 @@ test_verify_one_file! {
     //} => Err(err) => assert_one_fails(err)
     } => Err(err) => assert_vir_error_msg(err, "Not supported: pattern containing both an or-pattern (|) and an if-guard")
 }
+
+test_verify_one_file! {
+    #[test] let_expr_not_supported verus_code! {
+        fn stuff(x: Option<u64>) {
+            let Some(y) = x
+            else {
+                loop { }
+            };
+        }
+    } => Err(err) => assert_vir_error_msg(err, "The verifier does not yet support the following Rust feature: let-else")
+}