Skip to content

C# backend not handling well module and datatype homonyms #5746

@MikaelMayer

Description

@MikaelMayer

Dafny version

4.4.0

Code to produce this issue

module State {

  datatype State = State

}

module Foo {

   import opened State

   const bar: State

   method Main() {
     print "Hello!\n";
  }
}

Command to run and resulting output

dafny run file.dfy

What happened?

Dafny program verifier finished with 0 verified, 0 errors
Errors compiling program into tmphiUhb8.tmp
source(5712,25): error CS0426: The type name '_IState' does not exist in the type 'State'

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

Windows

Metadata

Metadata

Assignees

Labels

difficulty: good-first-issueGood first issuesinvalid translated codeThe compiler generates invalid code, making the the target language infrastructure crashkind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labellang: c#Dafny's C# transpiler and its runtime

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions