Skip to content

Rust code generation with --rust-module-name #5864

@ajewellamz

Description

@ajewellamz

Dafny version

4.8.1 (nightly)

Code to produce this issue

any

Command to run and resulting output

dafny -t rs

What happened?

Normally, dafny produces something like this at the top of implementation_from_dafny

pub mod aes_gcm;
pub mod _dafny_externs {
  pub use crate::aes_gcm::*;
}

When compiling with --rust-module-name the same thing is produced, where it should only produce

pub mod _dafny_externs {
  pub use crate::aes_gcm::*;
}

because otherwise it's referring to implementation_from_dafny::aes_gcm which does not exist.

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

Mac

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