Symex propagation: add output function #3527
Conversation
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d179716).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93545942
| @@ -780,3 +782,11 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const | |||
| } | |||
| } | |||
| } | |||
|
|
|||
| void goto_symex_statet::output_propagation_map(std::ostream &out) | |||
There was a problem hiding this comment.
Documentation appreciated, otherwise there's a risk that this will be removed as unused in the next clean up.
smowton
force-pushed
the
smowton/feature/symex-propagation-output
branch
from
d179716 to
f85c8b1
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: f85c8b1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94113136
|
I only have some minor comments |
|
@romainbrenguier what are they? :) |
| @@ -67,6 +67,7 @@ class goto_symex_statet final | |||
|
|
|||
| // Map L1 names to (L2) constants | |||
| std::map<irep_idt, exprt> propagation; | |||
| void output_propagation_map(std::ostream &); | |||
There was a problem hiding this comment.
This doesn't access any private field so it should be a static function (ideally taking a map as input).
There was a problem hiding this comment.
The field really ought to be private though (it's only used by goto_symext functions, and could/should be hidden), so I'm inclined to leave this as-is
| @@ -67,6 +67,7 @@ class goto_symex_statet final | |||
|
|
|||
| // Map L1 names to (L2) constants | |||
| std::map<irep_idt, exprt> propagation; | |||
| void output_propagation_map(std::ostream &); | |||
There was a problem hiding this comment.
Add documentation saying this is used for debugging
Another debugging widget for symex