-
Notifications
You must be signed in to change notification settings - Fork 259
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
Extending a trait with an opaque function causes error, but only on the commandline and not on VSCode. #4205
Comments
I add this as a way to simplify boogie debugging, especially in cases when VSCode is not consistent with the command-line like in #4205 I did not add any test for that as it's meant for Dafny development only, but I tested it manually. I borrowed the code from the driver.
I was able to look at the generated boogie code from the language server and the CLI. Here are the differences: VSCode => CLI implementation {:verboseName "F.bar (override check)"} OverrideCheck$$_module.F.bar(this: ref)
{
var F_$_Frame: <beta>[ref,Field beta]bool;
// initialize fuel constant
assume AsFuelBottom(StartFuel__module.F.bar) == StartFuel__module.F.bar;
assume AsFuelBottom(StartFuelAssert__module.F.bar) == StartFuelAssert__module.F.bar;
assert true;
- F_$_Frame := lambda#0(null, $Heap, alloc, false);
+ F_$_Frame := (lambda<alpha> $o: ref, $f: Field alpha ::
+ $o != null && read($Heap, $o, alloc) ==> false);
assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> false);
} Also, in a lot of other places, I see diffs like this, where VSCode emits an equivalence sign, and CLI emits an // #requires axiom for _module.F.bar
axiom (forall $ly: LayerType, this: ref ::
{ _module.F.bar#requires($ly, this) }
this != null && $Is(this, Tclass._module.F())
- ==> (_module.F.bar#requires($ly, this) <==> true));
+ ==> _module.F.bar#requires($ly, this) == true); |
But the problem is not in the comparison above. The CLI generates an extra boogie file that VSCode does not, which is suffixed with _module. I guess it's the exported version of the module.
|
I add this as a way to simplify boogie debugging, especially in cases when VSCode is not consistent with the command-line like in #4205 I did not add any test for that as it's meant for Dafny development only, but I tested it manually. I borrowed the code from the driver. Should I still list it as a feature? <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Dafny version
4.1.0
Code to produce this issue
Command to run and resulting output
What happened?
In the Boogie translation, the
override axiom for _module.T.bar in class _module.F
seems to have thereveal
argument missing.Lines 2955 to 2962 of boogie_print.bpl:
Whereas, lines 2810-2811:
The text was updated successfully, but these errors were encountered: