Skip to content

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
Collaborator

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
Collaborator

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