Introduce union tag type #2697
Introduce union tag type #2697
Conversation
src/goto-symex/goto_symex_state.cpp
Outdated
| type=symbol.type; | ||
| rename(type, l1_identifier, ns, level); | ||
| } | ||
| else if(type.id()==ID_struct_tag) |
There was a problem hiding this comment.
That's beyond what's claimed in the commit message.
src/goto-symex/rewrite_union.cpp
Outdated
| static bool have_to_rewrite_union( | ||
| const exprt &expr, | ||
| const namespacet &ns) | ||
| static bool have_to_rewrite_union(const exprt &expr) |
There was a problem hiding this comment.
This commit should really be in a separate pull request. It's likely the second commit that breaks things, while this one ought to have no impact at all. Also: the commit message could be much clearer because all that happens is removing the unused namespace parameter.
kroening
force-pushed
the
union_tag
branch
4 times, most recently
from
36888b6 to
d43ed19
Compare
kroening
force-pushed
the
union_tag
branch
3 times, most recently
from
d7da536 to
2b5277e
Compare
|
I've turned the last commit into a separate PR (#2915). |
| @@ -135,6 +135,7 @@ void cpp_typecheckt::typecheck_compound_type( | |||
| cpp_scopet *dest_scope=nullptr; | |||
| bool has_body=type.find(ID_body).is_not_nil(); | |||
| bool tag_only_declaration=type.get_bool(ID_C_tag_only_declaration); | |||
| bool is_union=type.id()==ID_union; | |||
There was a problem hiding this comment.
const and clang-format style spacing
src/ansi-c/c_typecheck_type.cpp
Outdated
| union_tag_typet tag_type(identifier); | ||
| tag_type.add_source_location() = type.source_location(); | ||
|
|
||
| c_qualifierst original_qualifiers(type); |
There was a problem hiding this comment.
This seems common to both branches and could be done beforehand.
src/ansi-c/c_typecheck_type.cpp
Outdated
|
|
||
| c_qualifierst original_qualifiers(type); | ||
| type.swap(tag_type); | ||
| original_qualifiers.write(type); |
There was a problem hiding this comment.
This seems common to both branches and could be done afterwards.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 2b5277e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84111556
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).
|
The TG failure is worrying. Otherwise it would be ready to go and unblock #2915. |
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 7f12c59).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84113136
This replaces the overloaded use of ID_symbol for union tags.