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.

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

JavaScript and Go backend: Incorrect map cardinality #5552

Open
khemichew opened this issue Jun 12, 2024 · 1 comment
Open

JavaScript and Go backend: Incorrect map cardinality #5552

khemichew opened this issue Jun 12, 2024 · 1 comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: golang Dafny's transpiler to Go and its runtime 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 priority: not yet Will reconsider working on this when we're looking for work

Comments

@khemichew
Copy link

Dafny version

4.6.0

Code to produce this issue

method Main() {
 print | map c : char | c in "oxasa" :: c := false |;
}

Command to run and resulting output

Output (for JavaScript and Go): 5
Output (for Python and C#): 4

What happened?

The output for the above should be 4 due to the duplication of 2 'a's of the map keyset; this example has been tested against the nightly version.

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

Linux

@khemichew khemichew added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Jun 12, 2024
@stefan-aws
Copy link
Collaborator

I can confirm the problem. Related: #5557.

@stefan-aws stefan-aws added lang: js Dafny's JavaScript transpiler and its runtime lang: golang Dafny's transpiler to Go and its runtime priority: unknown part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: not yet Will reconsider working on this when we're looking for work and removed priority: unknown labels Jun 17, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: golang Dafny's transpiler to Go and its runtime 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 priority: not yet Will reconsider working on this when we're looking for work
Projects
None yet
Development

No branches or pull requests

2 participants