C++: use struct tag instead of symbol_type #3060
Conversation
kroening
commented
Sep 28, 2018
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- My contribution is formatted in line with CODING_STANDARD.md.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
kroening
force-pushed
the
cpp-struct_tag
branch
from
7128f26 to
66c428b
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 7128f26).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86346729
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 66c428b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86348447
kroening
force-pushed
the
cpp-struct_tag
branch
from
66c428b to
2165f29
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 2165f29).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86362376
src/cpp/cpp_typecheck_bases.cpp
Outdated
| @@ -67,6 +70,8 @@ void cpp_typecheckt::typecheck_compound_bases(struct_typet &type) | |||
| throw 0; | |||
| } | |||
|
|
|||
| base_symbol_expr.type().id(ID_symbol_type); | |||
There was a problem hiding this comment.
That seems redundant? I don't think there is any way we could get here with base_symbol_expr.type().id() != ID_symbol_type.
There was a problem hiding this comment.
Indeed, turned into invariant.
kroening
force-pushed
the
cpp-struct_tag
branch
from
2165f29 to
a15fd5f
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: a15fd5f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86394591
kroening
force-pushed
the
cpp-struct_tag
branch
2 times, most recently
from
2a044d7 to
eed5246
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: eed5246).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86707663
kroening
force-pushed
the
cpp-struct_tag
branch
from
eed5246 to
114e4aa
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 114e4aa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86902083
kroening
force-pushed
the
cpp-struct_tag
branch
from
114e4aa to
8d06e52
Compare
src/cpp/cpp_typecheck_bases.cpp
Outdated
| @@ -67,6 +70,10 @@ void cpp_typecheckt::typecheck_compound_bases(struct_typet &type) | |||
| throw 0; | |||
| } | |||
|
|
|||
| DATA_INVARIANT( | |||
| base_symbol_expr.type().id() == ID_symbol_type, | |||
| "base classes are identified using symbol_types"); | |||
There was a problem hiding this comment.
I'm still confused: in line 57 there is a to_symbol_type, and none of the code that's between lines 57 and this one touches base_symbol_expr.
There was a problem hiding this comment.
Indeed, the invariant is unneeded, will remove.
kroening
force-pushed
the
cpp-struct_tag
branch
from
8d06e52 to
d2f803a
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 8d06e52).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87022823
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: d2f803a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87025201
