Skip to content

Comments have weird effects #159

@TheodoreEhrenborg

Description

@TheodoreEhrenborg

(I realize this probably isn't going to get fixed, based on the Non-Future Work section in the readme)

verusfmt sometimes wraps lines weirdly (e.g. == 0 below), and this seems to happen when there are comments nearby

use vstd::prelude::*;

verus! {

pub open spec fn foo(bytes: &[u8; 32]) -> bool {
    bytes[0] & bytes[0]
        == 0
    // A medium-length comment, only about 55 char long

}

pub open spec fn bar(bytes: &[u8; 32]) -> bool {
    bytes[0] & bytes[0] == 0
    // A shorter comment, only about 49 char long

}

} // verus!

This is using verusfmt main@upstream c105cf50 Add escape char support (#157)

Metadata

Metadata

Assignees

No one assigned

    Labels

    pr appreciatedIssues where a fixing PR is welcome; may be more difficult than "good first issue" tag

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions