Remove unnecessary copy and loss of state information #5778
Conversation
TGWDB
requested review from
kroening,
peterschrammel,
romainbrenguier,
smowton and
tautschnig
as code owners
src/goto-symex/goto_state.h
Outdated
| @@ -20,6 +20,9 @@ Author: Romain Brenguier, [email protected] | |||
|
|
|||
| #include "renaming_level.h" | |||
|
|
|||
| // 20210122 Forward declaration required | |||
There was a problem hiding this comment.
We generally don't date comments, in favour of using git blame / praise. Maybe we should but at the moment we don't
There was a problem hiding this comment.
Also, why is it required? It doesn't look necessary if you are deleting the code that uses it...
There was a problem hiding this comment.
Updated the comment to remove the date stamp. Also added more detail to the comment about the declaration of the child class inside the parent class. The parent class explicitly uses the child class, this was resolved before by declaring the constructor for the child class inline. I don't know why the child class needs to be used in the parent, this just removes the duplicate constructor declaration and handles the required (forward) declaration.
There was a problem hiding this comment.
Thank you for these updates, but can we please actually dig a little deeper here? It seems the apply_condition function is what uses goto_symex_statet, but then either 1) apply_condition could safely be used with a goto_statet instead of a goto_symex_statet, or 2) apply_condition should become a member function of goto_symex_statet instead of being a member of goto_statet. Thanks!
There was a problem hiding this comment.
The apply_condition code in goto_statet has special cases related to goto_symex_statet that are non-trivial to split from the parent class. To do this properly is a larger refactor that impacts several locations in the code and there are already comments related to this (e.g. see symex_goto.cpp lines 35-46).
I'm not comfortable taking on this larger refactor at the moment, specially since this PR is just to remove some redundant code.
Codecov Report
@@ Coverage Diff @@
## develop #5778 +/- ##
===========================================
- Coverage 69.54% 69.54% -0.01%
===========================================
Files 1243 1243
Lines 100701 100697 -4
===========================================
- Hits 70037 70033 -4
Misses 30664 30664
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
|
It may also be useful to add some history to the commit message: this constructor became obsolete as of 7938cd1. |
This commit removes an inline constructor that performed a copy of the state and thus could cause state information to be lost.
TGWDB
force-pushed
the
goto_statet_oddity
branch
from
b3288be to
c1938dc
Compare
This removes a constructor that was not necessary
because it implemented the default behaviour of
the copy constructor (and thus created two places
to edit if changes were made to the class).