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

Cpp tests failing betr branch #26

Open
JackMenandCameron opened this issue Apr 22, 2021 · 1 comment
Open

Cpp tests failing betr branch #26

JackMenandCameron opened this issue Apr 22, 2021 · 1 comment

Comments

@JackMenandCameron
Copy link
Collaborator

JackMenandCameron commented Apr 22, 2021

Betr branch is failing on the following tests

Failed Tests (4):
Dafny :: c++/class.dfy
Dafny :: c++/datatypes.dfy
Dafny :: c++/generic.dfy
Dafny :: c++/maps.dfy

Reasons

Type inference

Maps.dfy is not verifying correctly.

(114,24): Error: value does not satisfy the subset constraints of 'map<MyClass, uint32>'
Execution trace:
    (0,0): anon0

I am not sure but this seems to be an error in inferring the type. If the type is explicitly stated as
map<MyClass?, uint32> then the file verifies (this also works on main though it is not necessary).

Null vs NULL vs Nil vs 0 vs 0x0 vs .....

Seems that dafny stopped printing null values as 0 and now prints them as 0x0?

-jack wendy 0
-jack 0 0
+jack wendy 0x0
+jack 0x0 0x0
 ronald ronald 0
 1 1 1 0
-jack wendy 0
-jack 0 0
+jack wendy 0x0
+jack 0x0 0x0

This is also an issue at dafny-lang/dafny.

@parno
Copy link

parno commented Jun 17, 2021

The NULL issue is on track to be fixed in official Dafny: dafny-lang#1242

I'm not sure why type inference is behaving differently here. For now, I'm tempted to say that we should just add the explicit type annotation.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants