Skip to content

Conversation

ShashankVM
Copy link

Fixes #1287

@ShashankVM
Copy link
Author

ShashankVM commented Oct 3, 2025

Hi Project Maintainers!

I've been using EBMC for hobby projects for a year now. The VCD file generation for each cover statement was a feature that I sorely missed in my projects.

I've implemented this feature and verified it is working locally. I've attached the screenshot of the results.
image

I'm looking forward to contributing to this project and welcome feedback!

@kroening
Copy link
Collaborator

kroening commented Oct 4, 2025

This regresses on the current behavior, where you can get the trace in a file named as the argument of --vcd. The user still needs to give an argument to the --vcd switch, which will be ignored.

@ShashankVM
Copy link
Author

Thanks for your feedback. @kroening

Do we want to keep the argument for VCD filename?

If yes, I can include the filename argument as a suffix in the final filename.

If not, I can work on modifying the command line parsing logic. Please let me know how to proceed.

@kroening
Copy link
Collaborator

kroening commented Oct 7, 2025

Thanks for your feedback. @kroening

Do we want to keep the argument for VCD filename?

If yes, I can include the filename argument as a suffix in the final filename.

This is what we are doing for --random-traces (look at random_traces.cpp, line 169).

However, making that change would still regress the current behaviour. I am not opposed to this in principle, but we'd need to do this as part of a major version release. Let's do it.

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

Successfully merging this pull request may close these issues.

Generate VCD for each trace of cover property

2 participants