Linking: replace conflicting pointer types when one declaration is extern #2024
Conversation
tautschnig
requested review from
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel and
smowton
as code owners
tautschnig
force-pushed
the
extern-linking
branch
from
760202c to
c8dc07a
Compare
tautschnig
force-pushed
the
extern-linking
branch
from
c8dc07a to
252d815
Compare
tautschnig
force-pushed
the
extern-linking
branch
from
252d815 to
e1b62b9
Compare
tautschnig
force-pushed
the
extern-linking
branch
from
e1b62b9 to
d847b6c
Compare
| // versions of Visual Studio insist to use this in their C library | ||
| warning().source_location = symbol.value.find_source_location(); | ||
| warning() << "`extern' symbol should not have an initializer" << eom; | ||
| } | ||
| } |
There was a problem hiding this comment.
Turn into error when in gcc or clang mode?
src/util/replace_symbol.cpp
Outdated
| @@ -29,7 +29,8 @@ void replace_symbolt::insert( | |||
|
|
|||
| bool replace_symbolt::replace( | |||
| exprt &dest, | |||
| const bool replace_with_const) const | |||
| const bool replace_with_const, | |||
| const bool ignore_type_change) const | |||
| { | |||
There was a problem hiding this comment.
I think this is getting to bizarre, and to linker specific. I'd make that a separate piece of code, just for the linker.
tautschnig
force-pushed
the
extern-linking
branch
from
d847b6c to
5c8171f
Compare
tautschnig
force-pushed
the
extern-linking
branch
from
5c8171f to
3086f21
Compare
|
This is now implemented on top of #2723 with the suggested, linker-specific implementation. |
tautschnig
force-pushed
the
extern-linking
branch
3 times, most recently
from
6b111a4 to
6a20f61
Compare
tautschnig
force-pushed
the
extern-linking
branch
from
6a20f61 to
cbd5d9f
Compare
tautschnig
force-pushed
the
extern-linking
branch
from
cbd5d9f to
6e921c2
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 6e921c2).
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).
tautschnig
force-pushed
the
extern-linking
branch
from
6e921c2 to
c720555
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 6e921c2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/83986092
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: c720555).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84011100
tautschnig
force-pushed
the
extern-linking
branch
from
c720555 to
e8b03a7
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: e8b03a7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84094002
tautschnig
force-pushed
the
extern-linking
branch
from
e8b03a7 to
d7dae29
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: d7dae29).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86154692
|
@kroening ping? |
tautschnig
force-pushed
the
extern-linking
branch
from
d7dae29 to
2f60e13
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 2f60e13).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86766275
tautschnig
force-pushed
the
extern-linking
branch
from
2f60e13 to
80ff4e5
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 80ff4e5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86776976
No description provided.