Skip to content

Fail to Parse: slice range indexing #199

Closed
#229
Closed
Fail to Parse: slice range indexing#199
#229
Assignees
jaybosamiya-mscopilot-swe-agent

Description

@bsdinis
bsdinis
opened on May 27, 2026

Hello.

Given this piece of code:

  use vstd::prelude::*;

  verus! {
      fn slice_stuff(buffer: &[u8; 1024], n: usize) {
          foo(&buffer[..n]);
      }

      fn foo(buffer: &[u8]) {

      }
  }

verusfmt (0.7.0) fails to parse the range indexing:

Error:   × Failed to parse
   ╭─[src/fmt.rs:5:21]
 4 │     fn slice_stuff(buffer: &[u8; 1024], n: usize) {
 5 │         foo(&buffer[..n]);
   ·                     ┬
   ·                     ╰── here
 6 │     }
   ╰────
  help: Expected one of: COMMENT, expr

Activity

  1. jaybosamiya-ms commented on May 30, 2026

    @jaybosamiya-ms
    jaybosamiya-ms
    on May 30, 2026
    Collaborator

    Thanks for the bug report!

    I'm guessing that the prioritization order of the range_expr in expr_outer and related places is not set right in the PEG parser. Let's see if an agent figures out the fix.

  2. jaybosamiya-ms
    assigned
    Copilot
    and
    jaybosamiya-ms
    on May 30, 2026
  3. Copilot
    linked a pull request that will close this issueFix: Parse slice range indexing (e.g. `buffer[..n]`, `buffer[..=n]`) #201on May 30, 2026
  4. jaybosamiya-ms
    closed this as completedin #229on Sep 25, 2026

  5. bsdinis commented on Sep 28, 2026

    @bsdinis
    bsdinis
    on Sep 28, 2026
    Author

    Thank you!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions