Skip to content

Prepare DECL/DEAD construction with location #6420

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

Add new constructors to code_{decl,dead}t that also take a location.
This will help avoid some *_nonconst() calls. To facilitate this,
an additional make_dead instruction builder is also needed (which just
mirrors what we already have for other instruction types).

  • 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.
  • n/a 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).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Add new constructors to code_{decl,dead}t that also take a location.
This will help avoid some *_nonconst() calls. To facilitate this,
an additional make_dead instruction builder is also needed (which just
mirrors what we already have for other instruction types).
@kroening
Copy link
Member

This has a subtle problem: the location isn't supposed to go into the _code member any more, but into the _source_location member.

@tautschnig
Copy link
Collaborator Author

This has a subtle problem: the location isn't supposed to go into the _code member any more, but into the _source_location member.

I suppose we need to document this somewhere? Perhaps, however, this PR makes for a simpler transition as all those places can be spotted more easily?

@codecov
Copy link

codecov bot commented Oct 29, 2021

Codecov Report

Merging #6420 (c58a207) into develop (f6fa03c) will not change coverage.
The diff coverage is 100.00%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #6420   +/-   ##
========================================
  Coverage    75.98%   75.98%           
========================================
  Files         1524     1524           
  Lines       164299   164299           
========================================
  Hits        124843   124843           
  Misses       39456    39456           
Impacted Files Coverage Δ
src/goto-programs/goto_instruction_code.h 100.00% <ø> (ø)
src/goto-programs/goto_program.h 89.76% <100.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 ce2680b...c58a207. Read the comment docs.

@kroening
Copy link
Member

Sure, simply fix those two new constructors, and it's good to go!

@tautschnig
Copy link
Collaborator Author

Closing as the new constructors shouldn't be necessary as indicated in the discussion.

@tautschnig tautschnig closed this Nov 3, 2021
@tautschnig tautschnig deleted the decl-dead-constructors branch November 3, 2021 12:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants