Define an add_const utility function #4257
Merged
Conversation
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
romainbrenguier
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
romainbrenguier
force-pushed
the
feature/add-const
branch
from
67bada7 to
2c2228d
Compare
tautschnig
approved these changes
Feb 22, 2019
src/goto-symex/goto_symex_state.cpp
Outdated
| @@ -345,10 +347,12 @@ void goto_symex_statet::rename( | |||
|
|
|||
| INVARIANT( | |||
| (expr.id() != ID_with || | |||
| expr.type() == to_with_expr(expr).old().type()) && | |||
| add_const(expr).type() == to_with_expr(add_const(expr)).old().type()) && | |||
There was a problem hiding this comment.
Maybe declare a const exprt &c_expr = expr; before the INVARIANT and use that in here? There are a lot of add_consts here.
romainbrenguier
force-pushed
the
feature/add-const
branch
from
2c2228d to
58d6d9c
Compare
|
Simply use |
|
|
It seems you'd need |
This is useful in particular when we want to force the const version of a method to be called. For exprt there can be differences in performance between const and non-const.
In some places the non const version of .type() and others would be called. We force the const version to be called by using as_const. In the example in `jbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5` this reduced the number of calls to detach from 744638 to 736844.
romainbrenguier
force-pushed
the
feature/add-const
branch
from
58d6d9c to
32af11e
Compare
done |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This is useful in particular when we want to force the const version of
a method to be called.
For
exprtthere can be differences in performance between const andnon-const.
This is applied to
goto_symex_statet::renameas an example, and trying of the example injbmc/regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5it reduced the number of calls to detach from 744638 to 736844.