Define and use an expr_skeletont class #4841
Conversation
romainbrenguier
requested review from
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
This clarifies the meaning of skeletons, which we use in assignmentt. This makes sure the skeleton field is always of the correct form for a skeleton.
romainbrenguier
force-pushed
the
refactor/expr_skeleton
branch
from
c0d6745 to
c852e72
Compare
smowton
left a comment
smowton
left a comment
There was a problem hiding this comment.
I note all uses of compose and remove_op0 go together, combine them into one method compose(exprt)?
I'm not sure I would like that because it's hiding the fact that the first operand of the expression is discarded. To be clear it would have to be named something like |
smowton
left a comment
smowton
left a comment
There was a problem hiding this comment.
OK, this is certainly better than the current code anyhow
thk123
left a comment
thk123
left a comment
There was a problem hiding this comment.
Personally think the name isn't very clear, but still more clear than using the nil_expr directly
| /// \ref expr_skeletont::apply). It can also be composed with another skeleton, | ||
| /// let say `☐.some_field` which would give the skeleton `☐.some_field[index]` | ||
| /// (see \ref expr_skeletont::compose). | ||
| class expr_skeletont final |
There was a problem hiding this comment.
💡 I wouldn't have guessed the behaviour of this expression from the name. Perhaps algebraic_expr, partial_expr expr_template?
There was a problem hiding this comment.
Yes I couldn't find a very good name, but algebraic_expr could be mistaken for a special type of exprt (like expr containing symbols), expr_template would be expected to be a template, partial_expr is as good as expr_skeleton I think.
|
|
||
| /// Replace the missing part of the current skeleton by another skeleton, | ||
| /// ending in a bigger skeleton corresponding to the two combined. | ||
| expr_skeletont compose(expr_skeletont other) const; |
There was a problem hiding this comment.
Seems like this would be very easy and worthwhile to unit test
There was a problem hiding this comment.
I will add them in another pull request #4843 because it takes a lot of tries to get CI to pass these days.
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: c852e72).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/117093045
| exprt full_lhs2 = nil_exprt{}; | ||
| full_lhs.type() = int_type; | ||
| symex_assign.assign_symbol(ssa_foo, full_lhs2, rhs2, guard); | ||
| symex_assign.assign_symbol(ssa_foo, expr_skeletont{}, rhs2, guard); |
There was a problem hiding this comment.
I know I'm late to the party, but how is this equivalent to the previous code? The previous code had a type assigned. @romainbrenguier ?
5 participants
This clarifies the meaning of skeletons, which we use in assignmentt.
This makes sure the skeleton field is always of the correct form for a
skeleton.