You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If a discriminator has an underscore in it, Dafny generates invalid C# code. The method name will have that underscore replaced with two underscores, but any call to that method will have the underscore unchanged. This problem doesn't exist in Dafny release 3.2.0, but does exist in 3.3.0 and in the current version.
One can reproduce this and get the following error:
(1876,15): error CS1061: 'D' does not contain a definition for 'is_D_1' and no accessible extension method 'is_D_1' accepting a first argument of type 'D' could be found (are you missing a using directive or an assembly reference?)
by running Dafny on a file with the following contents:
module M {
datatype D = D_1(i: int) | D_2(b: bool)
method DoIt (d: D)
{
if (d.D_1?) {
print d.i;
}
else {
print d.b;
}
}
}
Running Dafny with /spillTargetCode:3 further illuminates the issue. One can see that the method is defined as:
public bool is_D__1 { get { return this is D_D__1; } }
but the call to that method is:
if ((d).is_D_1) {
The text was updated successfully, but these errors were encountered:
jaylorch
added
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
lang: c#
Dafny's C# transpiler and its runtime
labels
Nov 24, 2021
If a discriminator has an underscore in it, Dafny generates invalid C# code. The method name will have that underscore replaced with two underscores, but any call to that method will have the underscore unchanged. This problem doesn't exist in Dafny release 3.2.0, but does exist in 3.3.0 and in the current version.
One can reproduce this and get the following error:
by running Dafny on a file with the following contents:
Running Dafny with
/spillTargetCode:3
further illuminates the issue. One can see that the method is defined as:but the call to that method is:
The text was updated successfully, but these errors were encountered: