Simplify lhs before passing to symex_assign #34
Conversation
tautschnig
force-pushed
the
simplify-lhs
branch
from
c88863d to
4ee6d72
Compare
src/goto-symex/symex_assign.cpp
Outdated
| @@ -36,6 +36,14 @@ void goto_symext::symex_assign_rec( | |||
| code_assignt deref_code=code; | |||
|
|
|||
| clean_expr(deref_code.lhs(), state, true); | |||
| // make the structure of the lhs as simple as possible to avoid, | |||
There was a problem hiding this comment.
This comment may be better placed in the Purpose section function since this might not be the only place it would get called
There was a problem hiding this comment.
Hmm, just a brief question about your comment: what do you refer to as "it" when saying "it would get called?"
There was a problem hiding this comment.
Apologies for the delay in responding. It refers to the function do_simplify. I believe this comment to be explaining this function (all the way down to line 45).
|
The one risk tied to this proposed commit is that there is a strict requirement that the simplifier must not introduce dereference operations. |
|
@tautschnig, can we add an assertion so that we notice when the simplifier might be doing that (in future)? |
tautschnig
force-pushed
the
simplify-lhs
branch
from
4ee6d72 to
c20a7aa
Compare
|
@tautschnig What is the status of this PR, are you planning to add an assertion as suggested by @peterschrammel? |
|
My apologies for keeping this one on the backlog: yes, I do intend to add this assertion as suggested. I'll try to get this done as soon as possible. |
|
@peterschrammel @forejtv Assertion added as suggested - apologies for taking forever to implement a 1-line (plus comments) change. |
tautschnig
force-pushed
the
simplify-lhs
branch
2 times, most recently
from
8d33efa to
9c2f68b
Compare
tautschnig
force-pushed
the
simplify-lhs
branch
from
9c2f68b to
9b9b82b
Compare
Added missing .gitmodules file
|
I have rebased this again as it seemed like Travis had been using a vastly outdated configuration. |
This can help avoid some uses of byte_update, as the regression test shows.
|
@smowton @peterschrammel sorry to be a pain, but could you please re-review this PR in #2230, and also point the TG bump over there? I couldn't find any way to make Travis use an up-to-date configuration, it seems to be stuck back in 2016... |
No description provided.