Skip to content

C++ backend prints NULL instead of null #4154

Open
@robin-aws

Description

@robin-aws

Dafny version

4.1.0

Code to produce this issue

class C {}

method Main() {
  var n: C? := null;
  print n, "\n";
}

Command to run and resulting output

% dafny run -t:cs src/Scratch.dfy --unicode-char:false

Dafny program verifier finished with 0 verified, 0 errors
null
% dafny run -t:cpp src/Scratch.dfy --unicode-char:false

Dafny program verifier finished with 0 verified, 0 errors
NULL

What happened?

Even better, if you print null directly without given the null value a more precise type, you get nullptr.

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:` labellang: c++Dafny's C++ transpiler and its runtimetesting-method: uniform-backend-testingIssues found by ensuring uniform testing across backends

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions