Skip to content

Default value for external generic types #6049

Open
@momvart

Description

@momvart

The C++ translator assumes there's a get_XXXX_default() for each external type.

return String.Format("{1}::get_{0}_default()", IdProtect(udt.Name), udt.ResolvedClass.EnclosingModuleDefinition.GetCompileName(Options));

While this works for non-generic types, for generic ones, even if such implementation exists, it still requires the generic (template) parameters to be passed to it.

For example:

type {:extern "struct"} XXXX<T>

class A {
   var x: XXXX<B>
}

The generated code will be:

class A {
XXXX<B> x = get_XXXX_default();
}

If we provide a default function like below:

template <typename T>
XXXX<T> get_XXXX_default() {
    // ...
}

the C++ compiler does not infer B at the call site, and complains.

The solution would be to provide B to the function call, or use the same get_default so the user specializes it for the external type.

Metadata

Metadata

Assignees

No one assigned

    Labels

    kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labellang: c++Dafny's C++ transpiler and its runtimepart: code-generationSupport for transpiling Dafny to another language. If relevant, add a `lang:` tag

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions