Skip to content

Standard Library serialization and deserialization error #6227

@MikaelMayer

Description

@MikaelMayer

Dafny version

latest-nightly

Code to produce this issue

@Test
  method SpecTest() {
    expect Std.JSON.Spec.EscapeUnicode(7) == "0007";
  }

Command to run and resulting output

dafny test on that code when importing the standard libraries
It returnes `"7   "` instead which is an error.
Also, putting an escape like `\u0007` at the end of a string literal fails to deserialize

What happened?

Needs to be fixed

What type of operating system are you experiencing the problem on?

Windows

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions