Remove multiple function assertion

[karkhaz]

This commit removes an assertion that triggers when multiple functions
get mangled to the same name when using the --export-file-local-symbols
flag to goto-cc.

This assertion was previously valid when compiling files one at a time, but
commit fcd1083 introduced the possibility of compiling and linking several
files at once. This is a problem when two source files both include an
implementation file, like [1], because the implementation may contain static
functions that get mangled twice.

This commit replaces the assertion with a debug message in case users would
like to check how often this happens.

This commit fixes #5380.

[1] https://github.com/awslabs/aws-c-common/blob/master/include/aws/common/atomics_gnu.inl

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• 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.

[martin-cs]

As I understand emplace, the log will only be triggered if you have two things that mangle to the same name and are identical, right? If so and we have a valid use-case where this can happen (and it seems that #5398 has one) then this should be fine.

[karkhaz]

@martin-cs that's all correct. Thank you!

[codecov]

Codecov Report

Merging #5402 into develop will decrease coverage by 0.00%.
The diff coverage is 33.33%.

@@             Coverage Diff             @@
##           develop    #5402      +/-   ##
===========================================
- Coverage    68.19%   68.19%   -0.01%     
===========================================
  Files         1176     1176              
  Lines        97517    97519       +2     
===========================================
  Hits         66502    66502              
- Misses       31015    31017       +2     

Flag	Coverage Δ
#cproversmt2	42.73% <ø> (ø)
#regression	65.37% <33.33%> (-0.01%)	⬇️
#unit	32.24% <ø> (ø)

Impacted Files	Coverage Δ
src/goto-programs/name_mangler.h	96.00% <33.33%> (-4.00%)	⬇️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update faf7f43...599fd66. Read the comment docs.

[smowton]

Add a test?

[NlightNFotis]

LGTM

[NlightNFotis]

@karkhaz I think that's alright. I'd rather keep the test from the previous PR however, but now I can remove the backing out of the commit.

[NlightNFotis]

@smowton There's a test in #5398 that's relevant I believe.

[smowton]

ok

[smowton]

Hang on, surely in that case that test should change from broken to working or similar? Can we add a test that would previously trip the invariant?

[NlightNFotis]

@smowton The test is working because the #5398 is removing the commit that caused the issue in the first place. Assuming this goes in, the test should be passing.

If the test gets merged first, without first backing out the previous commit or just removing the assertion like in here, then it should fail. But the test is associated, it's just the merging sequence that should matter as to whether it passes or fails.

[NlightNFotis]

I am going ahead and merging this one. For any issues with this, ping me.