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

Abstract import of concrete module is allowed, produces invalid target code #5854

Open
ssomayyajula opened this issue Oct 23, 2024 · 0 comments
Labels
invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@ssomayyajula
Copy link
Contributor

Dafny version

latest

Code to produce this issue

module Concrete {
  method DoNothing() { }
}

abstract module Abstract {
  import C: Concrete
}

module MoreConcrete refines Abstract {
  
}

method Main() {
  MoreConcrete.C.DoNothing();
}

Command to run and resulting output

dafny run ...

error CS0103: The name 'Abstract' does not exist in the current context

What happened?

The abstract import of a concrete module should be disallowed.

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

Mac

@ssomayyajula ssomayyajula added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label invalid translated code The compiler generates invalid code, making the the target language infrastructure crash labels Oct 23, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Development

No branches or pull requests

1 participant