Subtypes of graph_nodet can override DOT output #2913
Conversation
karkhaz
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
karkhaz
force-pushed
the
kk-graph-pretty-nodes
branch
from
3e5d9b4 to
e1dcf60
Compare
src/util/graph.h
Outdated
| /// | ||
| /// If this function returns an empty string for a particular node, | ||
| /// grapht::output_dot() method will not output this node at all, nor any of | ||
| /// its incoming or outgoing edges. |
There was a problem hiding this comment.
Maybe use an optional type where the empty optional triggers this behavior. I'm not sure the actual behavior is exactly as describe, wouldn't we still output some edges which are coming into to these nodes?
There was a problem hiding this comment.
OK, I'm going to remove this from this PR and add a cleaner implementation in a different PR
src/util/graph.h
Outdated
| @@ -924,8 +960,14 @@ void grapht<N>::output_dot(std::ostream &out) const | |||
| for_each_successor(i, f); | |||
| }; | |||
|
|
|||
| const auto to_string = [](const node_indext &i) { return std::to_string(i); }; | |||
| output_dot_generic<node_indext>(out, for_each_node, for_each_succ, to_string); | |||
| const auto to_string = [&](const node_indext &i) { | |||
There was a problem hiding this comment.
why do we need this &?
There was a problem hiding this comment.
Thanks, I replaced the & with this, we do need to capture this.
src/util/graph.h
Outdated
| const std::string pretty = node_to_pretty(i); | ||
| if(pretty == "") | ||
| return; | ||
| out << pretty << ";\n"; | ||
| for_each_succ(i, [&](const node_index_type &n) { | ||
| out << node_to_string(i) << " -> " << node_to_string(n) << '\n'; |
There was a problem hiding this comment.
I think this will only produce a correct graph when pretty starts with the result of node_to_string. It would be better to enforce it in some way.
There was a problem hiding this comment.
Thanks, you're right. I've just pushed a cleaner implementation that enforces this.
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: e1dcf60).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84093354
karkhaz
force-pushed
the
kk-graph-pretty-nodes
branch
2 times, most recently
from
628986d to
324b68f
Compare
|
Some motivation for this PR. Before: |
src/util/graph.h
Outdated
| } | ||
|
|
||
| public: | ||
| std::string pretty(node_indext idx) const |
There was a problem hiding this comment.
node_indext could be const reference
src/util/graph.h
Outdated
| @@ -16,9 +16,11 @@ Author: Daniel Kroening, [email protected] | |||
| #include <cassert> | |||
| #include <functional> | |||
| #include <iosfwd> | |||
| #include <iostream> | |||
This commit introduces a virtual pretty() method to graph_nodet, whose default implementation has the same behaviour as before (only outputting the node's graph index with no attributes when dumped to a Graphviz DOT file). Subtypes of graph_nodet can override this method to provide a more informative representation of themselves when grapht::output_dot() is called.
karkhaz
force-pushed
the
kk-graph-pretty-nodes
branch
from
324b68f to
37fc17f
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 324b68f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84103467
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 628986d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84104004
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 37fc17f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84107718
|
Thank you @romainbrenguier, I applied your suggestions. All tests are passing. |
|
@peterschrammel not sure why you assigned me? I don't think I have access to merge this... |
This commit introduces a virtual pretty() method to graph_nodet, whose
default implementation has the same behaviour as before (only outputting
the node's graph index with no attributes when dumped to a Graphviz DOT
file). Subtypes of graph_nodet can override this method to provide a
more informative representation of themselves when grapht::output_dot()
is called.