Conversation
2 tasks
Was comparing loc with eloc.
Member
There was a problem hiding this comment.
I looked it over and it seems to make sense at first glance. Maybe it would be a good idea for someone else who is familiar with the ARGs (maybe @karoliineh?) to also take a look at this since I'm out of my depth here?
3 tasks
sim642
added a commit
to goblint/GobPie
that referenced
this pull request
May 27, 2024
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Like in #1462, I'm always afraid of doing any modifications in the ARG generation because it's very fragile and there have been no tests so far.
At some point I added https://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/scripts/sv-comp/witness-isomorphism.py to semi-automatically check if two sets of GraphML witnesses are isomorphic. But that requires a set of reference witnesses (which we don't have in the repository) and the networkx Python library that implements graph isomorphism algorithms.
This PR adds an alternative means of fully automatic tests for ARGs. This is similar to the CFG tests: a GraphViz graph is rendered as ASCII using
graph-easyand expected outputs are in the repository.The tests are very similar to Cram tests: if something changes, the tests will fail with a diff that can be promoted if intended. However, they aren't Cram tests but just dune expectation tests using rule generation.
The mechanism is somewhat complex (at least without dune 3.14), but nobody other than me will probably ever have to deal with these anyway (because they should just keep passing).
TODO
exp.arg→exp.arg.enabledGobPie#71.