Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Default JavaScript value for string malformed #5238

Closed
RustanLeino opened this issue Mar 22, 2024 · 0 comments · Fixed by #5239
Closed

Default JavaScript value for string malformed #5238

RustanLeino opened this issue Mar 22, 2024 · 0 comments · Fixed by #5239
Assignees
@RustanLeino
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: js Dafny's JavaScript transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag

Comments

@RustanLeino
Copy link
Collaborator

Dafny version

4.5.0

Code to produce this issue

method Main() {
  var s: seq<char>;
  s := *;
  print "(", s, ")\n";
}

Command to run and resulting output

% dafny run test.dfy --target=js

Dafny program verifier finished with 1 verified, 0 errors
[stdin]:1122
        throw e
        ^

TypeError: _0_s.toVerbatimString is not a function
    at Function.Main ([stdin]:1202:35)
    at [stdin]:1211:53
    at Object.$module.HandleHaltExceptions ([stdin]:1116:7)
    at [stdin]:1211:8
    at Script.runInThisContext (node:vm:131:12)
    at Object.runInThisContext (node:vm:308:38)
    at node:internal/process/execution:81:19
    at [stdin]-wrapper:6:22
    at evalScript (node:internal/process/execution:80:60)
    at node:internal/main/eval_stdin:29:5
(

What happened?

The JavaScript code generator has a special case for a seq<char> default value. Unfortunately, it gets it wrong.

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

Mac
@RustanLeino RustanLeino added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag lang: js Dafny's JavaScript transpiler and its runtime labels Mar 22, 2024
@RustanLeino RustanLeino self-assigned this Mar 22, 2024
RustanLeino added a commit to RustanLeino/dafny that referenced this issue Mar 22, 2024
@RustanLeino
fix: Generate proper default string value for JavaScript
87acd37 
Fixes dafny-lang#5238
@RustanLeino RustanLeino mentioned this issue Mar 22, 2024
Merged
RustanLeino added a commit that referenced this issue Mar 23, 2024
@RustanLeino
fix: Generate proper default string value for JavaScript (#5239)
f4fa255 
Fixes #5238


<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
RustanLeino added a commit to RustanLeino/dafny that referenced this issue Jun 8, 2024
@RustanLeino
fix: Generate proper default string value for JavaScript
9d8db7a 
Fixes dafny-lang#5238
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@RustanLeino RustanLeino

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: js Dafny's JavaScript transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Generate proper default string value for JavaScript RustanLeino/dafny
1 participant
@RustanLeino