Skip to content

Remove function from source_locationt [depends-on: #4131] #3514

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

Closed

Conversation

tautschnig
Copy link
Collaborator

A source location is a place in a text file, it does not have syntactic
information.

This is work in progress, known to require quite a bit more work to re-introduce the information about functions where needed. The current state also includes some additional hacks to detect where problems will arise.

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

@smowton
Copy link
Contributor

smowton commented Dec 3, 2018

Personally this seems like a step backwards -- a source location doesn't need to be a (row, col) coordinate, it seems appropriate for it to identify other source-code-level properties of a piece of codet or goto_programt::instructiont` data. What's the motivation for this?

@tautschnig
Copy link
Collaborator Author

We should discuss this with @kroening. Certainly it seems that at the moment there is considerable abuse of this information in the code base: anything stored in the source location should only be used for the purpose of reporting back to the user, and not affect program semantics. So maybe we keep it, but just clean up all usage.

@chrisr-diffblue
Copy link
Contributor

Is there scope to just modify the API (and then hence, the corresponding cleanup) so that it's API becomes 'store or output' only ?

@tautschnig
Copy link
Collaborator Author

Is there scope to just modify the API (and then hence, the corresponding cleanup) so that it's API becomes 'store or output' only ?

Sounds like a good idea to me. Yet I don't recall whether in a discussion with @kroening we had more reasons for the change, it's a while ago. So, @kroening, input much appreciated.

@tautschnig tautschnig force-pushed the remove-source-loc-function branch 3 times, most recently from f68080d to 696f443 Compare February 8, 2019 10:51
A source location is a place in a text file, and the function information stored
in there need not coincide with the name we use in the goto model.

Part 1: label_properties should use the actual function name so that properties
in different instantiations of a function (as may happen when linking static
functions) get unique names.
A source location is a place in a text file, and the function information stored
in there need not coincide with the name we use in the goto model.

Part 2: Wherever we generate fresh symbols or function-specific objects we
should use the actual function name to ensure fewer name collisions (for fresh
symbols) or actually unique objects.
…ion()

Even though we use it as an index into a data structure, ambiguity is not a
problem here.
This user-level heuristics is no more or less reliable than the file-name test
that's also used here.
None of the existing flags (nor any combination thereof) would enable us to
distinguish procedure-local type declarations from translation-unit wide ones.
@tautschnig tautschnig changed the title Remove function from source_locationt Remove function from source_locationt [depends-on: #4131] Feb 12, 2019
@tautschnig tautschnig force-pushed the remove-source-loc-function branch from 696f443 to 8d162bb Compare December 27, 2020 08:48
@TGWDB
Copy link
Contributor

TGWDB commented May 3, 2023

Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants