Skip to content

Do not error on undefined external linker symbols #7621

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Mar 28, 2023

Conversation

karkhaz
Copy link
Collaborator

@karkhaz karkhaz commented Mar 27, 2023

goto-cc currently parses the linker script given by the -T flag to find addresses for variables that are extern-declared in C files but not given a definition. This is because some variables are defined in the linker script, not in C code, and reading these definitions from the linker script is necessary to verify the C program.

Prior to this commit, goto-cc would error out if some extern-defined variables remained undefined even after reading the linker script. There is actually a valid use case for having undefined symbols even after linking, see this (search for "Undefined symbol to cause link failure"):

https://lore.kernel.org/all/[email protected]/T/

This commit turns the error into a warning and synthesizes a null pointer for such symbols.

  • 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.

@karkhaz karkhaz force-pushed the kk-warn-on-undefined-symbol branch from 0c70358 to bdc7c6c Compare March 27, 2023 13:42
@karkhaz karkhaz requested a review from tautschnig March 27, 2023 13:43
@karkhaz karkhaz force-pushed the kk-warn-on-undefined-symbol branch 3 times, most recently from daf3381 to 559ff8b Compare March 27, 2023 14:13
Copy link
Contributor

@harmim harmim left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would wrap the commit message body at 72 characters. It would be more consistent with other CBMC's commits.

@codecov
Copy link

codecov bot commented Mar 27, 2023

Codecov Report

Patch coverage has no change and project coverage change: -0.01 ⚠️

Comparison is base (9f894ae) 78.51% compared to head (b40be48) 78.50%.

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #7621      +/-   ##
===========================================
- Coverage    78.51%   78.50%   -0.01%     
===========================================
  Files         1671     1671              
  Lines       191845   191847       +2     
===========================================
  Hits        150618   150618              
- Misses       41227    41229       +2     
Impacted Files Coverage Δ
src/goto-cc/linker_script_merge.cpp 78.53% <0.00%> (-0.39%) ⬇️
src/goto-cc/linker_script_merge.h 100.00% <ø> (ø)

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

goto-cc currently parses the linker script given by the -T flag to find
addresses for variables that are extern-declared in C files but not
given a definition. This is because some variables are defined in the
linker script, not in C code, and reading these definitions from the
linker script is necessary to verify the C program.

Prior to this commit, goto-cc would error out if some extern-defined
variables remained undefined even after reading the linker script. There
is actually a valid use case for having undefined symbols even after
linking, see this (search for "Undefined symbol to cause link failure"):

    https://lore.kernel.org/all/[email protected]/T/

This commit turns the error into a warning and synthesizes a null
pointer for such symbols.
@karkhaz karkhaz force-pushed the kk-warn-on-undefined-symbol branch from 559ff8b to 9d1445c Compare March 27, 2023 15:28
@karkhaz karkhaz force-pushed the kk-warn-on-undefined-symbol branch from 9d1445c to b40be48 Compare March 27, 2023 15:30
@tautschnig tautschnig marked this pull request as ready for review March 28, 2023 10:21
@tautschnig tautschnig merged commit 98bba8e into diffblue:develop Mar 28, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants