-
Notifications
You must be signed in to change notification settings - Fork 257
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
Handle --coverage-report
with dafny translate
(or legacy compilation option)
#4965
Comments
Correct me if I'm wrong, but this is particularly tricky because you don't just have a few C# files to pass into |
That's correct, yes. |
|
I'm referring to this feature: 4d7bdf5 I think it's referenced here: http:https://dafny.org/dafny/DafnyRef/DafnyRef#sec-dafny-test |
--coverage-report
with dafny translate
(or legacy compilation option)--verification-coverage-report
with dafny translate
(or legacy compilation option)
--verification-coverage-report
with dafny translate
(or legacy compilation option)--coverage-report
with dafny translate
(or legacy compilation option)
Ah, I see. Sorry for my mistake! I was looking at Dafny 4.3 options. |
I think what we can do is change |
Summary
Currently there is no way to generate coverage report with separately compiled Dafny.
Background and Motivation
To compile tests, I call (legacy)
dafny -spillTargetCode:3 -out:/some/runtime/folder -runAllTests:1 ...
and run it with
dotnet run ...
This does not enable passing in the option
--coverage-report
. Callingdafny test DafnyFile.dfy
is difficult since the{:extern}
functions need to be linked via some fiddly C# compilation configuration.Proposed Feature
We propose adding the ability for
dafny -spillTargetCode:3
ordafny translate cs
(ideally the former for now) to handle the--coverage-report
flag, which would behave as if one calleddafny test --coverage-report:some-folder
directly, when running the emitted code withdotnet run
.Alternatives
I'm not sure what the alternative is, possibly enabling linking C#
extern
s more easily in thedafny test
configuration.The text was updated successfully, but these errors were encountered: