Skip to content

C++ compilation error on a datatype with a type parameter #1294

Open
@fpoli

Description

@fpoli

The C++ code generated by the following program doesn't compile.

Command: dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp Program.dfy

Program:

newtype nat32 = i:int | 0 <= i < 0x80000000

datatype PhantomData<T> = PhantomData(value: T)

method Main() {
    var x: nat32 := 123;
    var p := PhantomData(x);
}

Output:

Dafny program verifier finished with 2 verified, 0 errors
Wrote textual form of target program to Comp.cpp
Additional target code written to Comp.h
Comp.cpp:30:34: error: use of undeclared identifier 'T'
    _13_p = _module::PhantomData<T>(_12_x);
                                 ^
1 error generated.
Error while compiling C++ files. Process exited with exit code 1

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 runtimepriority: not yetWill reconsider working on this when we're looking for work

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions